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)

the Charact of U0 . x = (Opers (U1,B)) . x by A1, A2, Th4;

hence the Charact of U0 = Opers (U1,B) ; :: thesis: verum

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

for x being object st x in the carrier' of S holds
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;(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

the Charact of U0 . x = (Opers (U1,B)) . x by A1, A2, Th4;

hence the Charact of U0 = Opers (U1,B) ; :: thesis: verum