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

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

then H1 is_epimorphism U2,U1 by A3;

hence H1 is_isomorphism U2,U1 by A9; :: thesis: verum

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

then
H1 is "1-1"
;
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;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

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

then
H1 is "onto"
;
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;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

then H1 is_epimorphism U2,U1 by A3;

hence H1 is_isomorphism U2,U1 by A9; :: thesis: verum