let I be set ; :: thesis: for A, B being V2() 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 )

let A, B be V2() ManySortedSet of I; :: thesis: 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 )

let H be ManySortedFunction of A,B; :: thesis: 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 )

let H1 be ManySortedFunction of B,A; :: thesis: ( H is "1-1" & H is "onto" & H1 = H "" implies ( H ** H1 = id B & H1 ** H = id A ) )
assume that
A1: ( H is "1-1" & H is "onto" ) and
A2: H1 = H "" ; :: thesis: ( H ** H1 = id B & H1 ** H = id A )
A3: now :: thesis: for i being set st i in I holds
(H ** H1) . i = id (B . i)
let i be set ; :: thesis: ( i in I implies (H ** H1) . i = id (B . i) )
assume A4: i in I ; :: thesis: (H ** H1) . i = id (B . i)
then reconsider h = H . i as Function of (A . i),(B . i) by PBOOLE:def 15;
reconsider h1 = H1 . i as Function of (B . i),(A . i) by ;
i in dom H by ;
then A5: h is one-to-one by A1;
h1 = h " by A1, A2, A4, Def4;
then h * h1 = id (rng h) by ;
then h * h1 = id (B . i) by A1, A4;
hence (H ** H1) . i = id (B . i) by ; :: thesis: verum
end;
for i being set st i in I holds
(H1 ** H) . i = id (A . i)
proof
let i be set ; :: thesis: ( i in I implies (H1 ** H) . i = id (A . i) )
assume A6: i in I ; :: thesis: (H1 ** H) . i = id (A . i)
then reconsider h = H . i as Function of (A . i),(B . i) by PBOOLE:def 15;
reconsider h1 = H1 . i as Function of (B . i),(A . i) by ;
i in dom H by ;
then A7: h is one-to-one by A1;
( h1 = h " & dom h = A . i ) by ;
then h1 * h = id (A . i) by ;
hence (H1 ** H) . i = id (A . i) by ; :: thesis: verum
end;
hence ( H ** H1 = id B & H1 ** H = id A ) by ; :: thesis: verum