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 ;
A3: B0 is opers_closed by ;
reconsider B1 = the Sorts of U1 as MSSubset of U2 by ;
A4: B1 is opers_closed by ;
reconsider B19 = B1 as MSSubset of U1 by PBOOLE:def 18;
A5: the Charact of U1 = Opers (U2,B1) by ;
the Sorts of U0 is MSSubset of U1 by ;
then A6: the Sorts of U0 c= the Sorts of U1 by PBOOLE:def 18;
the Sorts of U1 is MSSubset of U2 by ;
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 ;
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 ;
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
let o be OperSymbol of S; :: thesis:
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
.= o /. B1 by Def8
.= (Den (o,U2)) | (((B1 #) * the Arity of S) . o) by ;
A13: ((B0 #) * the Arity of S) . o c= ((B19 #) * the Arity of S) . o by ;
Den (o,U0) = (Opers (U1,B0)) . o by
.= o /. B0 by Def8
.= ((Den (o,U2)) | (((B1 #) * the Arity of S) . o)) | (((B0 #) * the Arity of S) . o) by
.= (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 ;
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;
hence B is opers_closed ; :: thesis: the Charact of U0 = Opers (U2,B)
for x being object st x in the carrier' of S holds
the Charact of U0 . x = (Opers (U2,B)) . x
proof
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
.= o /. B1 by Def8
.= (Den (o,U2)) | (((B1 #) * the Arity of S) . o) by ;
thus the Charact of U0 . x = o /. B0 by
.= ((Den (o,U2)) | (((B1 #) * the Arity of S) . o)) | (((B0 #) * the Arity of S) . o) by
.= (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
.= o /. B by
.= (Opers (U2,B)) . x by Def8 ; :: thesis: verum
end;
hence the Charact of U0 = Opers (U2,B) ; :: thesis: verum