let S be non empty non void ManySortedSign ; :: thesis: for U1, U2 being non-empty MSAlgebra over S
for H being ManySortedFunction of U1,U2
for H1 being ManySortedFunction of U2,U1 st H is_isomorphism U1,U2 & H1 = H "" holds
H1 is_isomorphism U2,U1
let U1, U2 be non-empty MSAlgebra over S; :: thesis: for H being ManySortedFunction of U1,U2
for H1 being ManySortedFunction of U2,U1 st H is_isomorphism U1,U2 & H1 = H "" holds
H1 is_isomorphism U2,U1
let H be ManySortedFunction of U1,U2; :: thesis: for H1 being ManySortedFunction of U2,U1 st H is_isomorphism U1,U2 & H1 = H "" holds
H1 is_isomorphism U2,U1
let H1 be ManySortedFunction of U2,U1; :: thesis: ( H is_isomorphism U1,U2 & H1 = H "" implies H1 is_isomorphism U2,U1 )
assume that
A1: H is_isomorphism U1,U2 and
A2: H1 = H "" ; :: thesis: H1 is_isomorphism U2,U1
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

proof

let i be set ; :: thesis: for g being Function st i in dom H1 & g = H1 . i holds
g is one-to-one
let g be Function; :: thesis: ( i in dom H1 & g = H1 . i implies g is one-to-one )
assume that
A6: i in dom H1 and
A7: g = H1 . i ; :: thesis: g is one-to-one
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: verum

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

proof

let i be set ; :: thesis: ( i in the carrier of S implies rng (H1 . i) = the Sorts of U1 . i )
assume A10: i in the carrier of S ; :: thesis: rng (H1 . i) = the Sorts of U1 . i
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: verum

end;

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