let I be set ; :: thesis: for A, B being ManySortedSet of I st A is_transformable_to B holds
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 ManySortedSet of I; :: thesis: ( A is_transformable_to B implies 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 ) )
assume A1: A is_transformable_to B ; :: 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
A2: ( H is "1-1" & H is "onto" ) and
A3: H1 = H "" ; :: thesis: ( H ** H1 = id B & H1 ** H = id A )
reconsider F1 = H ** H1 as ManySortedFunction of I ;

A4: 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 A5: 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 A5, PBOOLE:def 15;
i in dom H by A5, PARTFUN1:def 2;
then A6: h is one-to-one by A2;
h1 = h " by A2, A3, A5, MSUALG_3:def 4;
then h * h1 = id (rng h) by A6, FUNCT_1:39;
then h * h1 = id (B . i) by A2, A5;
hence (H ** H1) . i = id (B . i) by A5, MSUALG_3:2; :: thesis: verum

end;

now :: thesis: for i being object st i in I holds
F1 . i is Function of (B . i),(B . i)

let i be object ; :: thesis: ( i in I implies F1 . i is Function of (B . i),(B . i) )
assume i in I ; :: thesis: F1 . i is Function of (B . i),(B . i)
then F1 . i = id (B . i) by A4;
hence F1 . i is Function of (B . i),(B . i) ; :: thesis: verum

end;

then A7: F1 is ManySortedFunction of B,B by PBOOLE:def 15;
reconsider F = H1 ** H as ManySortedFunction of I ;
A8: 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 A9: 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 A9, PBOOLE:def 15;
i in dom H by A9, PARTFUN1:def 2;
then A10: h is one-to-one by A2;
( B . i = {} implies A . i = {} ) by A1, A9;
then A11: dom h = A . i by FUNCT_2:def 1;
h1 = h " by A2, A3, A9, MSUALG_3:def 4;
then h1 * h = id (A . i) by A10, A11, FUNCT_1:39;
hence (H1 ** H) . i = id (A . i) by A9, MSUALG_3:2; :: thesis: verum

end;

now :: thesis: for i being object st i in I holds
(H1 ** H) . i is Function of (A . i),(A . i)

let i be object ; :: thesis: ( i in I implies (H1 ** H) . i is Function of (A . i),(A . i) )
assume i in I ; :: thesis: (H1 ** H) . i is Function of (A . i),(A . i)
then (H1 ** H) . i = id (A . i) by A8;
hence (H1 ** H) . i is Function of (A . i),(A . i) ; :: thesis: verum

end;

then reconsider F = F as ManySortedFunction of A,A by PBOOLE:def 15;
F = id A by A8, MSUALG_3:def 1;
hence ( H ** H1 = id B & H1 ** H = id A ) by A4, A7, MSUALG_3:def 1; :: thesis: verum