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

for U1, U2 being MSSubAlgebra of U0 st the Sorts of U1 c= the Sorts of U2 holds

U1 is MSSubAlgebra of U2

let U0 be MSAlgebra over S; :: thesis: for U1, U2 being MSSubAlgebra of U0 st the Sorts of U1 c= the Sorts of U2 holds

U1 is MSSubAlgebra of U2

let U1, U2 be MSSubAlgebra of U0; :: thesis: ( the Sorts of U1 c= the Sorts of U2 implies U1 is MSSubAlgebra of U2 )

reconsider B1 = the Sorts of U1, B2 = the Sorts of U2 as MSSubset of U0 by Def9;

assume A1: the Sorts of U1 c= the Sorts of U2 ; :: thesis: U1 is MSSubAlgebra of U2

hence the Sorts of U1 is MSSubset of U2 by PBOOLE:def 18; :: according to MSUALG_2:def 9 :: thesis: for B being MSSubset of U2 st B = the Sorts of U1 holds

( B is opers_closed & the Charact of U1 = Opers (U2,B) )

let B be MSSubset of U2; :: thesis: ( B = the Sorts of U1 implies ( B is opers_closed & the Charact of U1 = Opers (U2,B) ) )

A2: B1 is opers_closed by Def9;

set O = the Charact of U1;

set P = Opers (U2,B);

A3: the Charact of U1 = Opers (U0,B1) by Def9;

A4: B2 is opers_closed by Def9;

A5: the Charact of U2 = Opers (U0,B2) by Def9;

assume A6: B = the Sorts of U1 ; :: thesis: ( B is opers_closed & the Charact of U1 = Opers (U2,B) )

A7: for o being OperSymbol of S holds B is_closed_on o

for x being object st x in the carrier' of S holds

the Charact of U1 . x = (Opers (U2,B)) . x

for U1, U2 being MSSubAlgebra of U0 st the Sorts of U1 c= the Sorts of U2 holds

U1 is MSSubAlgebra of U2

let U0 be MSAlgebra over S; :: thesis: for U1, U2 being MSSubAlgebra of U0 st the Sorts of U1 c= the Sorts of U2 holds

U1 is MSSubAlgebra of U2

let U1, U2 be MSSubAlgebra of U0; :: thesis: ( the Sorts of U1 c= the Sorts of U2 implies U1 is MSSubAlgebra of U2 )

reconsider B1 = the Sorts of U1, B2 = the Sorts of U2 as MSSubset of U0 by Def9;

assume A1: the Sorts of U1 c= the Sorts of U2 ; :: thesis: U1 is MSSubAlgebra of U2

hence the Sorts of U1 is MSSubset of U2 by PBOOLE:def 18; :: according to MSUALG_2:def 9 :: thesis: for B being MSSubset of U2 st B = the Sorts of U1 holds

( B is opers_closed & the Charact of U1 = Opers (U2,B) )

let B be MSSubset of U2; :: thesis: ( B = the Sorts of U1 implies ( B is opers_closed & the Charact of U1 = Opers (U2,B) ) )

A2: B1 is opers_closed by Def9;

set O = the Charact of U1;

set P = Opers (U2,B);

A3: the Charact of U1 = Opers (U0,B1) by Def9;

A4: B2 is opers_closed by Def9;

A5: the Charact of U2 = Opers (U0,B2) by Def9;

assume A6: B = the Sorts of U1 ; :: thesis: ( B is opers_closed & the Charact of U1 = Opers (U2,B) )

A7: for o being OperSymbol of S holds B is_closed_on o

proof

hence
B is opers_closed
; :: thesis: the Charact of U1 = Opers (U2,B)
let o be OperSymbol of S; :: thesis: B is_closed_on o

A8: B1 is_closed_on o by A2;

A9: B2 is_closed_on o by A4;

A10: Den (o,U2) = (Opers (U0,B2)) . o by A5, MSUALG_1:def 6

.= o /. B2 by Def8

.= (Den (o,U0)) | (((B2 #) * the Arity of S) . o) by A9, Def7 ;

Den (o,U1) = (Opers (U0,B1)) . o by A3, MSUALG_1:def 6

.= o /. B1 by Def8

.= (Den (o,U0)) | (((B1 #) * the Arity of S) . o) by A8, Def7

.= (Den (o,U0)) | ((((B2 #) * the Arity of S) . o) /\ (((B1 #) * the Arity of S) . o)) by A1, Th2, XBOOLE_1:28

.= (Den (o,U2)) | (((B1 #) * the Arity of S) . o) by A10, RELAT_1:71 ;

then rng ((Den (o,U2)) | (((B1 #) * the Arity of S) . o)) c= Result (o,U1) by RELAT_1:def 19;

then rng ((Den (o,U2)) | (((B1 #) * the Arity of S) . o)) c= ( the Sorts of U1 * the ResultSort of S) . o by MSUALG_1:def 5;

hence B is_closed_on o by A6; :: thesis: verum

end;A8: B1 is_closed_on o by A2;

A9: B2 is_closed_on o by A4;

A10: Den (o,U2) = (Opers (U0,B2)) . o by A5, MSUALG_1:def 6

.= o /. B2 by Def8

.= (Den (o,U0)) | (((B2 #) * the Arity of S) . o) by A9, Def7 ;

Den (o,U1) = (Opers (U0,B1)) . o by A3, MSUALG_1:def 6

.= o /. B1 by Def8

.= (Den (o,U0)) | (((B1 #) * the Arity of S) . o) by A8, Def7

.= (Den (o,U0)) | ((((B2 #) * the Arity of S) . o) /\ (((B1 #) * the Arity of S) . o)) by A1, Th2, XBOOLE_1:28

.= (Den (o,U2)) | (((B1 #) * the Arity of S) . o) by A10, RELAT_1:71 ;

then rng ((Den (o,U2)) | (((B1 #) * the Arity of S) . o)) c= Result (o,U1) by RELAT_1:def 19;

then rng ((Den (o,U2)) | (((B1 #) * the Arity of S) . o)) c= ( the Sorts of U1 * the ResultSort of S) . o by MSUALG_1:def 5;

hence B is_closed_on o by A6; :: thesis: verum

for x being object st x in the carrier' of S holds

the Charact of U1 . x = (Opers (U2,B)) . x

proof

hence
the Charact of U1 = Opers (U2,B)
; :: thesis: verum
let x be object ; :: thesis: ( x in the carrier' of S implies the Charact of U1 . x = (Opers (U2,B)) . x )

assume x in the carrier' of S ; :: thesis: the Charact of U1 . x = (Opers (U2,B)) . x

then reconsider o = x as OperSymbol of S ;

A11: B1 is_closed_on o by A2;

A12: B2 is_closed_on o by A4;

A13: Den (o,U2) = (Opers (U0,B2)) . o by A5, MSUALG_1:def 6

.= o /. B2 by Def8

.= (Den (o,U0)) | (((B2 #) * the Arity of S) . o) by A12, Def7 ;

thus the Charact of U1 . x = o /. B1 by A3, Def8

.= (Den (o,U0)) | (((B1 #) * the Arity of S) . o) by A11, Def7

.= (Den (o,U0)) | ((((B2 #) * the Arity of S) . o) /\ (((B1 #) * the Arity of S) . o)) by A1, Th2, XBOOLE_1:28

.= (Den (o,U2)) | (((B1 #) * the Arity of S) . o) by A13, RELAT_1:71

.= o /. B by A6, A7, Def7

.= (Opers (U2,B)) . x by Def8 ; :: thesis: verum

end;assume x in the carrier' of S ; :: thesis: the Charact of U1 . x = (Opers (U2,B)) . x

then reconsider o = x as OperSymbol of S ;

A11: B1 is_closed_on o by A2;

A12: B2 is_closed_on o by A4;

A13: Den (o,U2) = (Opers (U0,B2)) . o by A5, MSUALG_1:def 6

.= o /. B2 by Def8

.= (Den (o,U0)) | (((B2 #) * the Arity of S) . o) by A12, Def7 ;

thus the Charact of U1 . x = o /. B1 by A3, Def8

.= (Den (o,U0)) | (((B1 #) * the Arity of S) . o) by A11, Def7

.= (Den (o,U0)) | ((((B2 #) * the Arity of S) . o) /\ (((B1 #) * the Arity of S) . o)) by A1, Th2, XBOOLE_1:28

.= (Den (o,U2)) | (((B1 #) * the Arity of S) . o) by A13, RELAT_1:71

.= o /. B by A6, A7, Def7

.= (Opers (U2,B)) . x by Def8 ; :: thesis: verum