the Sorts of U2 is MSSubset of U0 by Def10;
then A1: the Sorts of U2 c= the Sorts of U0 by PBOOLE:def 23;
the Sorts of U1 is MSSubset of U0 by Def10;
then the Sorts of U1 c= the Sorts of U0 by PBOOLE:def 23;
then the Sorts of U1 /\ the Sorts of U2 c= the Sorts of U0 /\ the Sorts of U0 by A1, PBOOLE:23;
then reconsider A = the Sorts of U1 /\ the Sorts of U2 as MSSubset of U0 by PBOOLE:def 23;
reconsider E = U0 | A as strict MSSubAlgebra of U0 ;
take E ; :: thesis: ( the Sorts of E = the Sorts of U1 /\ the Sorts of U2 & ( for B being MSSubset of U0 st B = the Sorts of E holds
( B is opers_closed & the Charact of E = Opers U0,B ) ) )
A is opers_closed

proof

reconsider u1 = the Sorts of U1, u2 = the Sorts of U2 as MSSubset of U0 by Def10;
let o be OperSymbol of S; :: according to MSUALG_2:def 7 :: thesis: A is_closed_on o
A2: dom ((u1 # ) * the Arity of S) = the carrier' of S by PARTFUN1:def 4;
A3: dom ((u2 # ) * the Arity of S) = the carrier' of S by PARTFUN1:def 4;
u2 is opers_closed by Def10;
then u2 is_closed_on o by Def7;
then A4: rng ((Den o,U0) | (((u2 # ) * the Arity of S) . o)) c= (u2 * the ResultSort of S) . o by Def6;
dom ((A # ) * the Arity of S) = the carrier' of S by PARTFUN1:def 4;
then A5: ((A # ) * the Arity of S) . o = (A # ) . (the Arity of S . o) by FUNCT_1:22
.= (A # ) . (the_arity_of o) by MSUALG_1:def 6
.= product ((u1 /\ u2) * (the_arity_of o)) by PBOOLE:def 19
.= (product (u1 * (the_arity_of o))) /\ (product (u2 * (the_arity_of o))) by Th2
.= ((u1 # ) . (the_arity_of o)) /\ (product (u2 * (the_arity_of o))) by PBOOLE:def 19
.= ((u1 # ) . (the_arity_of o)) /\ ((u2 # ) . (the_arity_of o)) by PBOOLE:def 19
.= ((u1 # ) . (the Arity of S . o)) /\ ((u2 # ) . (the_arity_of o)) by MSUALG_1:def 6
.= ((u1 # ) . (the Arity of S . o)) /\ ((u2 # ) . (the Arity of S . o)) by MSUALG_1:def 6
.= (((u1 # ) * the Arity of S) . o) /\ ((u2 # ) . (the Arity of S . o)) by A2, FUNCT_1:22
.= (((u1 # ) * the Arity of S) . o) /\ (((u2 # ) * the Arity of S) . o) by A3, FUNCT_1:22 ;
then (Den o,U0) | (((A # ) * the Arity of S) . o) = ((Den o,U0) | (((u2 # ) * the Arity of S) . o)) | (((u1 # ) * the Arity of S) . o) by RELAT_1:100;
then rng ((Den o,U0) | (((A # ) * the Arity of S) . o)) c= rng ((Den o,U0) | (((u2 # ) * the Arity of S) . o)) by RELAT_1:99;
then A6: rng ((Den o,U0) | (((A # ) * the Arity of S) . o)) c= (u2 * the ResultSort of S) . o by A4, XBOOLE_1:1;
u1 is opers_closed by Def10;
then u1 is_closed_on o by Def7;
then A7: rng ((Den o,U0) | (((u1 # ) * the Arity of S) . o)) c= (u1 * the ResultSort of S) . o by Def6;
A8: dom (u2 * the ResultSort of S) = the carrier' of S by PARTFUN1:def 4;
(Den o,U0) | (((A # ) * the Arity of S) . o) = ((Den o,U0) | (((u1 # ) * the Arity of S) . o)) | (((u2 # ) * the Arity of S) . o) by A5, RELAT_1:100;
then rng ((Den o,U0) | (((A # ) * the Arity of S) . o)) c= rng ((Den o,U0) | (((u1 # ) * the Arity of S) . o)) by RELAT_1:99;
then rng ((Den o,U0) | (((A # ) * the Arity of S) . o)) c= (u1 * the ResultSort of S) . o by A7, XBOOLE_1:1;
then A9: rng ((Den o,U0) | (((A # ) * the Arity of S) . o)) c= ((u1 * the ResultSort of S) . o) /\ ((u2 * the ResultSort of S) . o) by A6, XBOOLE_1:19;
A10: dom (A * the ResultSort of S) = the carrier' of S by PARTFUN1:def 4;
dom (u1 * the ResultSort of S) = the carrier' of S by PARTFUN1:def 4;
then ((u1 * the ResultSort of S) . o) /\ ((u2 * the ResultSort of S) . o) = (u1 . (the ResultSort of S . o)) /\ ((u2 * the ResultSort of S) . o) by FUNCT_1:22
.= (u1 . (the ResultSort of S . o)) /\ (u2 . (the ResultSort of S . o)) by A8, FUNCT_1:22
.= (u1 . (the_result_sort_of o)) /\ (u2 . (the ResultSort of S . o)) by MSUALG_1:def 7
.= (u1 . (the_result_sort_of o)) /\ (u2 . (the_result_sort_of o)) by MSUALG_1:def 7
.= A . (the_result_sort_of o) by PBOOLE:def 8
.= A . (the ResultSort of S . o) by MSUALG_1:def 7
.= (A * the ResultSort of S) . o by A10, FUNCT_1:22 ;
hence A is_closed_on o by A9, Def6; :: thesis: verum

end;

then U0 | A = MSAlgebra(# A,(Opers U0,A) #) by Def16;
hence the Sorts of E = the Sorts of U1 /\ the Sorts of U2 ; :: thesis: for B being MSSubset of U0 st B = the Sorts of E holds
( B is opers_closed & the Charact of E = Opers U0,B )
thus for B being MSSubset of U0 st B = the Sorts of E holds
( B is opers_closed & the Charact of E = Opers U0,B ) by Def10; :: thesis: verum