theorem Th17: :: AUTALG_1:17

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