let I be set ; :: thesis:
let A, B be V2 ManySortedSet of I; :: thesis:
let H be ManySortedFunction of A,B; :: thesis:
let H1 be ManySortedFunction of B,A; :: thesis:
assume A1: ( H is "1-1" & H is "onto" & H1 = H "" ) ; :: thesis:
A2: for i being set st i in I holds
(H1 ** H) . i = id (A . i)

let i be set ; :: thesis:
assume A3: i in I ; :: thesis:
then A4: i in dom H by PBOOLE:def 3;
reconsider h = H . i as Function of A . i,B . i by A3, PBOOLE:def 18;
reconsider h1 = H1 . i as Function of B . i,A . i by A3, PBOOLE:def 18;
A5: h1 = h " by A1, A3, Def5;
A6: h is one-to-one by A1, A4, Def2;
( B . i = {} implies A . i = {} ) by A3;
then ( dom h = A . i & rng h c= B . i ) by FUNCT_2:def 1, RELSET_1:12;
then h1 * h = id (A . i) by A5, A6, FUNCT_1:61;
hence (H1 ** H) . i = id (A . i) by A3, Th2; :: thesis:

end;

now

let i be set ; :: thesis:
assume A7: i in I ; :: thesis:
then A8: i in dom H by PBOOLE:def 3;
reconsider h = H . i as Function of A . i,B . i by A7, PBOOLE:def 18;
reconsider h1 = H1 . i as Function of B . i,A . i by A7, PBOOLE:def 18;
A9: h1 = h " by A1, A7, Def5;
h is one-to-one by A1, A8, Def2;
then h * h1 = id (rng h) by A9, FUNCT_1:61;
then h * h1 = id (B . i) by A1, A7, Def3;
hence (H ** H1) . i = id (B . i) by A7, Th2; :: thesis:

end;

hence ( H ** H1 = id B & H1 ** H = id A ) by A2, Def1; :: thesis: