theorem Th12: :: AUTALG_1:12

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 "" is "1-1" & F "" is "onto" )