theorem Th11: :: AUTALG_1:11

for x being set
for A being ManySortedSet of {x} holds A = x .--> (A . x)