A2: the carrier of U1 /\ the carrier of U2 c= the carrier of U1 by XBOOLE_1:17;
the carrier of U1 is Subset of U0 by Def7;
then reconsider C = the carrier of U1 /\ the carrier of U2 as non empty Subset of U0 by A1, A2, XBOOLE_1:1;
set S = UAStr(# C,(Opers (U0,C)) #);
A3: the carrier of U1 /\ the carrier of U2 c= the carrier of U2 by XBOOLE_1:17;

A4: now :: thesis: for o being operation of U0 holds C is_closed_on o

let o be operation of U0; :: thesis: C is_closed_on o

now :: thesis: for s being FinSequence of C st len s = arity o holds
o . s in C

set B1 = the carrier of U1;
set B2 = the carrier of U2;
let s be FinSequence of C; :: thesis: ( len s = arity o implies o . s in C )
reconsider s2 = s as FinSequence of the carrier of U2 by A3, FINSEQ_2:24;
reconsider s1 = s as FinSequence of the carrier of U1 by A2, FINSEQ_2:24;
assume A5: len s = arity o ; :: thesis: o . s in C
reconsider B1 = the carrier of U1 as non empty Subset of U0 by Def7;
reconsider B2 = the carrier of U2 as non empty Subset of U0 by Def7;
B2 is opers_closed by Def7;
then B2 is_closed_on o ;
then A6: o . s2 in B2 by A5;
B1 is opers_closed by Def7;
then B1 is_closed_on o ;
then o . s1 in B1 by A5;
hence o . s in C by A6, XBOOLE_0:def 4; :: thesis: verum

end;

hence C is_closed_on o ; :: thesis: verum

end;

then A7: for B being non empty Subset of U0 st B = the carrier of UAStr(# C,(Opers (U0,C)) #) holds
( the charact of UAStr(# C,(Opers (U0,C)) #) = Opers (U0,B) & B is opers_closed ) ;
reconsider S = UAStr(# C,(Opers (U0,C)) #) as Universal_Algebra by Th14;
reconsider S = S as strict SubAlgebra of U0 by A7, Def7;
take S ; :: thesis: ( the carrier of S = the carrier of U1 /\ the carrier of U2 & ( for B being non empty Subset of U0 st B = the carrier of S holds
( the charact of S = Opers (U0,B) & B is opers_closed ) ) )
thus ( the carrier of S = the carrier of U1 /\ the carrier of U2 & ( for B being non empty Subset of U0 st B = the carrier of S holds
( the charact of S = Opers (U0,B) & B is opers_closed ) ) ) by A4; :: thesis: verum