the Sorts of U2 is MSSubset of U0 by Def9;
then A1: the Sorts of U2 c= the Sorts of U0 by PBOOLE:def 18;
the Sorts of U1 is MSSubset of U0 by Def9;
then the Sorts of U1 c= the Sorts of U0 by PBOOLE:def 18;
then the Sorts of U1 (/\) the Sorts of U2 c= the Sorts of U0 (/\) the Sorts of U0 by A1, PBOOLE:21;
then reconsider A = the Sorts of U1 (/\) the Sorts of U2 as MSSubset of U0 by PBOOLE:def 18;
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 Def9;
let o be OperSymbol of S; :: according to MSUALG_2:def 6 :: thesis: A is_closed_on o
A2: dom ((u1 #) * the Arity of S) = the carrier' of S by PARTFUN1:def 2;
A3: dom ((u2 #) * the Arity of S) = the carrier' of S by PARTFUN1:def 2;
u2 is opers_closed by Def9;
then u2 is_closed_on o ;
then A4: rng ((Den (o,U0)) | (((u2 #) * the Arity of S) . o)) c= (u2 * the ResultSort of S) . o ;
dom ((A #) * the Arity of S) = the carrier' of S by PARTFUN1:def 2;
then A5: ((A #) * the Arity of S) . o = (A #) . ( the Arity of S . o) by FUNCT_1:12
.= (A #) . (the_arity_of o) by MSUALG_1:def 1
.= product ((u1 (/\) u2) * (the_arity_of o)) by FINSEQ_2:def 5
.= (product (u1 * (the_arity_of o))) /\ (product (u2 * (the_arity_of o))) by Th1
.= ((u1 #) . (the_arity_of o)) /\ (product (u2 * (the_arity_of o))) by FINSEQ_2:def 5
.= ((u1 #) . (the_arity_of o)) /\ ((u2 #) . (the_arity_of o)) by FINSEQ_2:def 5
.= ((u1 #) . ( the Arity of S . o)) /\ ((u2 #) . (the_arity_of o)) by MSUALG_1:def 1
.= ((u1 #) . ( the Arity of S . o)) /\ ((u2 #) . ( the Arity of S . o)) by MSUALG_1:def 1
.= (((u1 #) * the Arity of S) . o) /\ ((u2 #) . ( the Arity of S . o)) by A2, FUNCT_1:12
.= (((u1 #) * the Arity of S) . o) /\ (((u2 #) * the Arity of S) . o) by A3, FUNCT_1:12 ;
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:71;
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:70;
then A6: rng ((Den (o,U0)) | (((A #) * the Arity of S) . o)) c= (u2 * the ResultSort of S) . o by A4;
u1 is opers_closed by Def9;
then u1 is_closed_on o ;
then A7: rng ((Den (o,U0)) | (((u1 #) * the Arity of S) . o)) c= (u1 * the ResultSort of S) . o ;
A8: dom (u2 * the ResultSort of S) = the carrier' of S by PARTFUN1:def 2;
(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:71;
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:70;
then rng ((Den (o,U0)) | (((A #) * the Arity of S) . o)) c= (u1 * the ResultSort of S) . o by A7;
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 2;
dom (u1 * the ResultSort of S) = the carrier' of S by PARTFUN1:def 2;
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:12
.= (u1 . ( the ResultSort of S . o)) /\ (u2 . ( the ResultSort of S . o)) by A8, FUNCT_1:12
.= (u1 . (the_result_sort_of o)) /\ (u2 . ( the ResultSort of S . o)) by MSUALG_1:def 2
.= (u1 . (the_result_sort_of o)) /\ (u2 . (the_result_sort_of o)) by MSUALG_1:def 2
.= A . (the_result_sort_of o) by PBOOLE:def 5
.= A . ( the ResultSort of S . o) by MSUALG_1:def 2
.= (A * the ResultSort of S) . o by A10, FUNCT_1:12 ;
hence A is_closed_on o by A9; :: thesis: verum

end;

then U0 | A = MSAlgebra(# A,(Opers (U0,A)) #) by Def15;
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 Def9; :: thesis: verum