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 )

(H1 ** H) . i = id (A . 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)

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 A4, PBOOLE:def 15;

i in dom H by A4, PARTFUN1:def 2;

then A5: h is one-to-one by A1;

h1 = h " by A1, A2, A4, Def4;

then h * h1 = id (rng h) by A5, FUNCT_1:39;

then h * h1 = id (B . i) by A1, A4;

hence (H ** H1) . i = id (B . i) by A4, Th2; :: thesis: verum

end;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 A4, PBOOLE:def 15;

i in dom H by A4, PARTFUN1:def 2;

then A5: h is one-to-one by A1;

h1 = h " by A1, A2, A4, Def4;

then h * h1 = id (rng h) by A5, FUNCT_1:39;

then h * h1 = id (B . i) by A1, A4;

hence (H ** H1) . i = id (B . i) by A4, Th2; :: thesis: verum

(H1 ** H) . i = id (A . i)

proof

hence
( H ** H1 = id B & H1 ** H = id A )
by A3, Def1; :: thesis: verum
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 A6, PBOOLE:def 15;

i in dom H by A6, PARTFUN1:def 2;

then A7: h is one-to-one by A1;

( h1 = h " & dom h = A . i ) by A1, A2, A6, Def4, FUNCT_2:def 1;

then h1 * h = id (A . i) by A7, FUNCT_1:39;

hence (H1 ** H) . i = id (A . i) by A6, Th2; :: thesis: verum

end;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 A6, PBOOLE:def 15;

i in dom H by A6, PARTFUN1:def 2;

then A7: h is one-to-one by A1;

( h1 = h " & dom h = A . i ) by A1, A2, A6, Def4, FUNCT_2:def 1;

then h1 * h = id (A . i) by A7, FUNCT_1:39;

hence (H1 ** H) . i = id (A . i) by A6, Th2; :: thesis: verum