for x being set
for A being FinSequence st x in rng A holds
( A <- x in dom A & x = A . (A <- x) )