let S be non empty non void ManySortedSign ; :: thesis: for U1 being MSAlgebra over S holds

( id the Sorts of U1 is_isomorphism U1,U1 & U1,U1 are_isomorphic )

let U1 be MSAlgebra over S; :: thesis: ( id the Sorts of U1 is_isomorphism U1,U1 & U1,U1 are_isomorphic )

A1: id the Sorts of U1 is_homomorphism U1,U1 by Th9;

for i being set

for f being Function st i in dom (id the Sorts of U1) & (id the Sorts of U1) . i = f holds

f is one-to-one

then A4: id the Sorts of U1 is_monomorphism U1,U1 by A1;

for i being set st i in the carrier of S holds

rng ((id the Sorts of U1) . i) = the Sorts of U1 . i

then A5: id the Sorts of U1 is_epimorphism U1,U1 by A1;

hence id the Sorts of U1 is_isomorphism U1,U1 by A4; :: thesis: U1,U1 are_isomorphic

take id the Sorts of U1 ; :: according to MSUALG_3:def 11 :: thesis: id the Sorts of U1 is_isomorphism U1,U1

thus id the Sorts of U1 is_isomorphism U1,U1 by A4, A5; :: thesis: verum

( id the Sorts of U1 is_isomorphism U1,U1 & U1,U1 are_isomorphic )

let U1 be MSAlgebra over S; :: thesis: ( id the Sorts of U1 is_isomorphism U1,U1 & U1,U1 are_isomorphic )

A1: id the Sorts of U1 is_homomorphism U1,U1 by Th9;

for i being set

for f being Function st i in dom (id the Sorts of U1) & (id the Sorts of U1) . i = f holds

f is one-to-one

proof

then
id the Sorts of U1 is "1-1"
;
let i be set ; :: thesis: for f being Function st i in dom (id the Sorts of U1) & (id the Sorts of U1) . i = f holds

f is one-to-one

let f be Function; :: thesis: ( i in dom (id the Sorts of U1) & (id the Sorts of U1) . i = f implies f is one-to-one )

assume that

A2: i in dom (id the Sorts of U1) and

A3: (id the Sorts of U1) . i = f ; :: thesis: f is one-to-one

i in the carrier of S by A2, PARTFUN1:def 2;

then f = id ( the Sorts of U1 . i) by A3, Def1;

hence f is one-to-one ; :: thesis: verum

end;f is one-to-one

let f be Function; :: thesis: ( i in dom (id the Sorts of U1) & (id the Sorts of U1) . i = f implies f is one-to-one )

assume that

A2: i in dom (id the Sorts of U1) and

A3: (id the Sorts of U1) . i = f ; :: thesis: f is one-to-one

i in the carrier of S by A2, PARTFUN1:def 2;

then f = id ( the Sorts of U1 . i) by A3, Def1;

hence f is one-to-one ; :: thesis: verum

then A4: id the Sorts of U1 is_monomorphism U1,U1 by A1;

for i being set st i in the carrier of S holds

rng ((id the Sorts of U1) . i) = the Sorts of U1 . i

proof

then
id the Sorts of U1 is "onto"
;
let i be set ; :: thesis: ( i in the carrier of S implies rng ((id the Sorts of U1) . i) = the Sorts of U1 . i )

assume i in the carrier of S ; :: thesis: rng ((id the Sorts of U1) . i) = the Sorts of U1 . i

then (id the Sorts of U1) . i = id ( the Sorts of U1 . i) by Def1;

hence rng ((id the Sorts of U1) . i) = the Sorts of U1 . i ; :: thesis: verum

end;assume i in the carrier of S ; :: thesis: rng ((id the Sorts of U1) . i) = the Sorts of U1 . i

then (id the Sorts of U1) . i = id ( the Sorts of U1 . i) by Def1;

hence rng ((id the Sorts of U1) . i) = the Sorts of U1 . i ; :: thesis: verum

then A5: id the Sorts of U1 is_epimorphism U1,U1 by A1;

hence id the Sorts of U1 is_isomorphism U1,U1 by A4; :: thesis: U1,U1 are_isomorphic

take id the Sorts of U1 ; :: according to MSUALG_3:def 11 :: thesis: id the Sorts of U1 is_isomorphism U1,U1

thus id the Sorts of U1 is_isomorphism U1,U1 by A4, A5; :: thesis: verum