for X being non empty set
for x being set holds the_value_of (X --> x) = x