let S be non empty non void ManySortedSign ; :: thesis: for U0, U1, U2 being MSAlgebra over S st U0 is MSSubAlgebra of U1 & U1 is MSSubAlgebra of U2 holds

U0 is MSSubAlgebra of U2

let U0, U1, U2 be MSAlgebra over S; :: thesis: ( U0 is MSSubAlgebra of U1 & U1 is MSSubAlgebra of U2 implies U0 is MSSubAlgebra of U2 )

assume that

A1: U0 is MSSubAlgebra of U1 and

A2: U1 is MSSubAlgebra of U2 ; :: thesis: U0 is MSSubAlgebra of U2

reconsider B0 = the Sorts of U0 as MSSubset of U1 by A1, Def9;

A3: B0 is opers_closed by A1, Def9;

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

A4: B1 is opers_closed by A2, Def9;

reconsider B19 = B1 as MSSubset of U1 by PBOOLE:def 18;

A5: the Charact of U1 = Opers (U2,B1) by A2, Def9;

the Sorts of U0 is MSSubset of U1 by A1, Def9;

then A6: the Sorts of U0 c= the Sorts of U1 by PBOOLE:def 18;

the Sorts of U1 is MSSubset of U2 by A2, Def9;

then the Sorts of U1 c= the Sorts of U2 by PBOOLE:def 18;

then the Sorts of U0 c= the Sorts of U2 by A6, PBOOLE:13;

hence the Sorts of U0 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 U0 holds

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

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

set O = the Charact of U0;

set P = Opers (U2,B);

A7: the Charact of U0 = Opers (U1,B0) by A1, Def9;

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

A9: 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 U0 . x = (Opers (U2,B)) . x

U0 is MSSubAlgebra of U2

let U0, U1, U2 be MSAlgebra over S; :: thesis: ( U0 is MSSubAlgebra of U1 & U1 is MSSubAlgebra of U2 implies U0 is MSSubAlgebra of U2 )

assume that

A1: U0 is MSSubAlgebra of U1 and

A2: U1 is MSSubAlgebra of U2 ; :: thesis: U0 is MSSubAlgebra of U2

reconsider B0 = the Sorts of U0 as MSSubset of U1 by A1, Def9;

A3: B0 is opers_closed by A1, Def9;

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

A4: B1 is opers_closed by A2, Def9;

reconsider B19 = B1 as MSSubset of U1 by PBOOLE:def 18;

A5: the Charact of U1 = Opers (U2,B1) by A2, Def9;

the Sorts of U0 is MSSubset of U1 by A1, Def9;

then A6: the Sorts of U0 c= the Sorts of U1 by PBOOLE:def 18;

the Sorts of U1 is MSSubset of U2 by A2, Def9;

then the Sorts of U1 c= the Sorts of U2 by PBOOLE:def 18;

then the Sorts of U0 c= the Sorts of U2 by A6, PBOOLE:13;

hence the Sorts of U0 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 U0 holds

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

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

set O = the Charact of U0;

set P = Opers (U2,B);

A7: the Charact of U0 = Opers (U1,B0) by A1, Def9;

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

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

proof

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

A10: B0 is_closed_on o by A3;

A11: B1 is_closed_on o by A4;

A12: Den (o,U1) = (Opers (U2,B1)) . o by A5, MSUALG_1:def 6

.= o /. B1 by Def8

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

A13: ((B0 #) * the Arity of S) . o c= ((B19 #) * the Arity of S) . o by A6, Th2;

Den (o,U0) = (Opers (U1,B0)) . o by A7, MSUALG_1:def 6

.= o /. B0 by Def8

.= ((Den (o,U2)) | (((B1 #) * the Arity of S) . o)) | (((B0 #) * the Arity of S) . o) by A10, A12, Def7

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

.= (Den (o,U2)) | (((B0 #) * the Arity of S) . o) by A13, XBOOLE_1:28 ;

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

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

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

end;A10: B0 is_closed_on o by A3;

A11: B1 is_closed_on o by A4;

A12: Den (o,U1) = (Opers (U2,B1)) . o by A5, MSUALG_1:def 6

.= o /. B1 by Def8

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

A13: ((B0 #) * the Arity of S) . o c= ((B19 #) * the Arity of S) . o by A6, Th2;

Den (o,U0) = (Opers (U1,B0)) . o by A7, MSUALG_1:def 6

.= o /. B0 by Def8

.= ((Den (o,U2)) | (((B1 #) * the Arity of S) . o)) | (((B0 #) * the Arity of S) . o) by A10, A12, Def7

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

.= (Den (o,U2)) | (((B0 #) * the Arity of S) . o) by A13, XBOOLE_1:28 ;

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

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

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

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

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

proof

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

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

then reconsider o = x as OperSymbol of S ;

A14: B0 is_closed_on o by A3;

A15: B1 is_closed_on o by A4;

A16: Den (o,U1) = (Opers (U2,B1)) . o by A5, MSUALG_1:def 6

.= o /. B1 by Def8

.= (Den (o,U2)) | (((B1 #) * the Arity of S) . o) by A15, Def7 ;

thus the Charact of U0 . x = o /. B0 by A7, Def8

.= ((Den (o,U2)) | (((B1 #) * the Arity of S) . o)) | (((B0 #) * the Arity of S) . o) by A14, A16, Def7

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

.= (Den (o,U2)) | (((B #) * the Arity of S) . o) by A6, A8, Th2, XBOOLE_1:28

.= o /. B by A9, Def7

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

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

then reconsider o = x as OperSymbol of S ;

A14: B0 is_closed_on o by A3;

A15: B1 is_closed_on o by A4;

A16: Den (o,U1) = (Opers (U2,B1)) . o by A5, MSUALG_1:def 6

.= o /. B1 by Def8

.= (Den (o,U2)) | (((B1 #) * the Arity of S) . o) by A15, Def7 ;

thus the Charact of U0 . x = o /. B0 by A7, Def8

.= ((Den (o,U2)) | (((B1 #) * the Arity of S) . o)) | (((B0 #) * the Arity of S) . o) by A14, A16, Def7

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

.= (Den (o,U2)) | (((B #) * the Arity of S) . o) by A6, A8, Th2, XBOOLE_1:28

.= o /. B by A9, Def7

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