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

proof

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;

then id the Sorts of U1 is "1-1" ;
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

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;

then id the Sorts of U1 is "onto" ;
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