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 ;
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:
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 #) . () by MSUALG_1:def 1
.= product ((u1 (/\) u2) * ()) by FINSEQ_2:def 5
.= (product (u1 * ())) /\ (product (u2 * ())) by Th1
.= ((u1 #) . ()) /\ (product (u2 * ())) by FINSEQ_2:def 5
.= ((u1 #) . ()) /\ ((u2 #) . ()) by FINSEQ_2:def 5
.= ((u1 #) . ( the Arity of S . o)) /\ ((u2 #) . ()) 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
.= (((u1 #) * the Arity of S) . o) /\ (((u2 #) * the Arity of S) . o) by ;
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 ;
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 ;
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
.= (u1 . ) /\ (u2 . ( the ResultSort of S . o)) by MSUALG_1:def 2
.= (u1 . ) /\ (u2 . ) by MSUALG_1:def 2
.= A . by PBOOLE:def 5
.= A . ( the ResultSort of S . o) by MSUALG_1:def 2
.= (A * the ResultSort of S) . o by ;
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