theorem Th5: :: MSUALG_3:5

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