let S be non empty non void ManySortedSign ; :: thesis:
let U1, U2 be non-empty MSAlgebra over S; :: thesis:
let H be ManySortedFunction of U1,U2; :: thesis:
let H1 be ManySortedFunction of U2,U1; :: thesis:
assume that
A1: H is_isomorphism U1,U2 and
A2: H1 = H "" ; :: thesis:
A3: H1 is_homomorphism U2,U1 by A1, A2, Lm2;
H is_monomorphism U1,U2 by A1;
then A4: H is "1-1" ;
H is_epimorphism U1,U2 by A1;
then A5: H is "onto" ;
for i being set
for g being Function st i in dom H1 & g = H1 . i holds
g is one-to-one

let i be set ; :: thesis:
let g be Function; :: thesis:
assume that
A6: i in dom H1 and
A7: g = H1 . i ; :: thesis:
A8: i in the carrier of S by A6, PARTFUN1:def 2;
then reconsider f = H . i as Function of ( the Sorts of U1 . i),( the Sorts of U2 . i) by PBOOLE:def 15;
i in dom H by A8, PARTFUN1:def 2;
then f is one-to-one by A4;
then f " is one-to-one ;
hence g is one-to-one by A2, A4, A5, A7, A8, Def4; :: thesis:

end;

then H1 is "1-1" ;
then A9: H1 is_monomorphism U2,U1 by A3;
for i being set st i in the carrier of S holds
rng (H1 . i) = the Sorts of U1 . i

let i be set ; :: thesis:
assume A10: i in the carrier of S ; :: thesis:
then reconsider f = H . i as Function of ( the Sorts of U1 . i),( the Sorts of U2 . i) by PBOOLE:def 15;
i in dom H by A10, PARTFUN1:def 2;
then f is one-to-one by A4;
then rng (f ") = dom f by FUNCT_1:33;
then rng (f ") = the Sorts of U1 . i by A10, FUNCT_2:def 1;
hence rng (H1 . i) = the Sorts of U1 . i by A2, A4, A5, A10, Def4; :: thesis:

end;

then H1 is "onto" ;
then H1 is_epimorphism U2,U1 by A3;
hence H1 is_isomorphism U2,U1 by A9; :: thesis: