let S be non empty non void ManySortedSign ; :: thesis: for U0, U1 being MSAlgebra over S st MSAlgebra(# the Sorts of U0, the Charact of U0 #) = MSAlgebra(# the Sorts of U1, the Charact of U1 #) holds
U0 is MSSubAlgebra of U1
let U0, U1 be MSAlgebra over S; :: thesis: ( MSAlgebra(# the Sorts of U0, the Charact of U0 #) = MSAlgebra(# the Sorts of U1, the Charact of U1 #) implies U0 is MSSubAlgebra of U1 )
assume A1: MSAlgebra(# the Sorts of U0, the Charact of U0 #) = MSAlgebra(# the Sorts of U1, the Charact of U1 #) ; :: thesis: U0 is MSSubAlgebra of U1
hence the Sorts of U0 is MSSubset of U1 by PBOOLE:def 18; :: according to MSUALG_2:def 9 :: thesis: for B being MSSubset of U1 st B = the Sorts of U0 holds
( B is opers_closed & the Charact of U0 = Opers (U1,B) )
let B be MSSubset of U1; :: thesis: ( B = the Sorts of U0 implies ( B is opers_closed & the Charact of U0 = Opers (U1,B) ) )
set f1 = the Charact of U0;
set f2 = Opers (U1,B);
assume A2: B = the Sorts of U0 ; :: thesis: ( B is opers_closed & the Charact of U0 = Opers (U1,B) )
thus B is opers_closed :: thesis: the Charact of U0 = Opers (U1,B)

proof

let o be OperSymbol of S; :: according to MSUALG_2:def 6 :: thesis: B is_closed_on o
(Den (o,U1)) | (((B #) * the Arity of S) . o) c= Den (o,U1) by RELAT_1:59;
then ( rng ((Den (o,U1)) | (((B #) * the Arity of S) . o)) c= rng (Den (o,U1)) & rng (Den (o,U1)) c= Result (o,U1) & Result (o,U1) = (B * the ResultSort of S) . o ) by A1, A2, MSUALG_1:def 5, RELAT_1:11, RELAT_1:def 19;
hence rng ((Den (o,U1)) | (((B #) * the Arity of S) . o)) c= (B * the ResultSort of S) . o ; :: according to MSUALG_2:def 5 :: thesis: verum

end;

for x being object st x in the carrier' of S holds
the Charact of U0 . x = (Opers (U1,B)) . x by A1, A2, Th4;
hence the Charact of U0 = Opers (U1,B) ; :: thesis: verum