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;

( 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

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

then A7:
for B being non empty Subset of U0 st B = the carrier of UAStr(# C,(Opers (U0,C)) #) holds let o be operation of U0; :: thesis: C is_closed_on o

end;now :: thesis: for s being FinSequence of C st len s = arity o holds

o . s in C

hence
C is_closed_on o
; :: thesis: verumo . 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;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

( 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