let S be non empty non void ManySortedSign ; 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; ( 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
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
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; U1,U1 are_isomorphic
take
id the Sorts of U1
; MSUALG_3:def 11 id the Sorts of U1 is_isomorphism U1,U1
thus
id the Sorts of U1 is_isomorphism U1,U1
by A4, A5; verum