Dear Yuri,
The best way for you to learn about sets and functions is to use the
Toolbox to see what the expressions you write mean. Just open a new
spec in it and just add an "EXTENDS Integers" statement. (You should
also add any other standard modules whose operators you want to use,
such as the Sequences module.) On the TLC Model Checker menu, open a
new model. In the _expression_ field, you can type a TLA+ _expression_
and click on the button with the white arrowhead in a green circle.
TLC will evaluate the _expression_ and print the result in the Value
field. For example, the result of evaluating the _expression_
{"a"} \union {"b"} is {"a", "b"}.
To see what { [x -> d] : x \in {1..n} } means, you need to choose some
"small" values for d and n -- for example {"a", "b"} and 3. Evaluate
{ [x -> {"a", "b"}] : x \in {1..3} } and then figure out why it equals
the result that TLC produces.
Leslie Lamport