theorem :: AUTALG_1:13

for I being set
for A, B being non-empty ManySortedSet of I
for F being ManySortedFunction of A,B st F is "1-1" & F is "onto" holds
(F "") "" = F