let U0, U1, U2 be Universal_Algebra; :: thesis: ( U0 is SubAlgebra of U1 & U1 is SubAlgebra of U2 implies U0 is SubAlgebra of U2 )
assume that
A1: U0 is SubAlgebra of U1 and
A2: U1 is SubAlgebra of U2 ; :: thesis: U0 is SubAlgebra of U2
A3: the carrier of U0 is Subset of U1 by A1, Def7;
reconsider B2 = the carrier of U1 as non empty Subset of U2 by A2, Def7;
A4: the charact of U1 = Opers (U2,B2) by A2, Def7;
the carrier of U1 is Subset of U2 by A2, Def7;
hence the carrier of U0 is Subset of U2 by A3, XBOOLE_1:1; :: according to UNIALG_2:def 7 :: thesis: for B being non empty Subset of U2 st B = the carrier of U0 holds
( the charact of U0 = Opers (U2,B) & B is opers_closed )
let B be non empty Subset of U2; :: thesis: ( B = the carrier of U0 implies ( the charact of U0 = Opers (U2,B) & B is opers_closed ) )
assume A5: B = the carrier of U0 ; :: thesis: ( the charact of U0 = Opers (U2,B) & B is opers_closed )
reconsider B1 = the carrier of U0 as non empty Subset of U1 by A1, Def7;
A6: the charact of U0 = Opers (U1,B1) by A1, Def7;
A7: B2 is opers_closed by A2, Def7;
A8: dom the charact of U1 = dom (Opers (U2,B2)) by A2, Def7
.= dom the charact of U2 by Def6 ;
A9: B1 is opers_closed by A1, Def7;

A10: now :: thesis: for o2 being operation of U2 holds B is_closed_on o2

let o2 be operation of U2; :: thesis: B is_closed_on o2
consider n being Nat such that
A11: n in dom the charact of U2 and
A12: the charact of U2 . n = o2 by FINSEQ_2:10;
A13: dom the charact of U2 = dom (Opers (U2,B2)) by Def6;
then reconsider o21 = the charact of U1 . n as operation of U1 by A4, A11, FUNCT_1:def 3;
A14: dom o21 = (arity o21) -tuples_on the carrier of U1 by MARGREL1:22;
A15: dom the charact of U1 = dom (Opers (U1,B1)) by Def6;
then reconsider o20 = the charact of U0 . n as operation of U0 by A6, A4, A11, A13, FUNCT_1:def 3;
A16: dom o20 = (arity o20) -tuples_on the carrier of U0 by MARGREL1:22;
A17: ( dom o2 = (arity o2) -tuples_on the carrier of U2 & dom (o2 | ((arity o2) -tuples_on B2)) = (dom o2) /\ ((arity o2) -tuples_on B2) ) by MARGREL1:22, RELAT_1:61;
A18: B2 is_closed_on o2 by A7;
A19: o21 = o2 /. B2 by A4, A11, A12, A13, Def6;
then o21 = o2 | ((arity o2) -tuples_on B2) by A18, Def5;
then A20: arity o2 = arity o21 by A14, A17, FINSEQ_2:110, MARGREL1:21;
A21: B1 is_closed_on o21 by A9;
A22: o20 = o21 /. B1 by A6, A4, A11, A13, A15, Def6;
then o20 = o21 | ((arity o21) -tuples_on B1) by A21, Def5;
then (arity o20) -tuples_on B1 = ((arity o21) -tuples_on the carrier of U1) /\ ((arity o21) -tuples_on B1) by A16, A14, RELAT_1:61;
then A23: arity o20 = arity o21 by FINSEQ_2:110, MARGREL1:21;

now :: thesis: for s being FinSequence of B st len s = arity o2 holds
o2 . s in B

let s be FinSequence of B; :: thesis: ( len s = arity o2 implies o2 . s in B )
reconsider s1 = s as Element of B1 * by A5, FINSEQ_1:def 11;
reconsider s0 = s as Element of the carrier of U0 * by A5, FINSEQ_1:def 11;
A24: rng o20 c= B by A5, RELAT_1:def 19;
rng s c= B by FINSEQ_1:def 4;
then rng s c= B2 by A3, A5, XBOOLE_1:1;
then s is FinSequence of B2 by FINSEQ_1:def 4;
then reconsider s2 = s as Element of B2 * by FINSEQ_1:def 11;
assume A25: len s = arity o2 ; :: thesis: o2 . s in B
then s2 in { w where w is Element of B2 * : len w = arity o2 } ;
then A26: s2 in (arity o2) -tuples_on B2 by FINSEQ_2:def 4;
s0 in { w where w is Element of the carrier of U0 * : len w = arity o20 } by A23, A20, A25;
then s0 in (arity o20) -tuples_on the carrier of U0 by FINSEQ_2:def 4;
then A27: o20 . s0 in rng o20 by A16, FUNCT_1:def 3;
s1 in { w where w is Element of B1 * : len w = arity o21 } by A20, A25;
then A28: s1 in (arity o21) -tuples_on B1 by FINSEQ_2:def 4;
o20 . s0 = (o21 | ((arity o21) -tuples_on B1)) . s1 by A21, A22, Def5
.= o21 . s1 by A28, FUNCT_1:49
.= (o2 | ((arity o2) -tuples_on B2)) . s2 by A18, A19, Def5
.= o2 . s by A26, FUNCT_1:49 ;
hence o2 . s in B by A27, A24; :: thesis: verum

end;

hence B is_closed_on o2 ; :: thesis: verum

end;

A29: dom the charact of U0 = dom (Opers (U1,B1)) by A1, Def7
.= dom the charact of U1 by Def6 ;
A30: dom the charact of U2 = dom (Opers (U2,B)) by Def6;
A31: B = B1 by A5;

now :: thesis: for n being Nat st n in dom (Opers (U2,B)) holds
(Opers (U2,B)) . n = the charact of U0 . n

let n be Nat; :: thesis: ( n in dom (Opers (U2,B)) implies (Opers (U2,B)) . n = the charact of U0 . n )
assume A32: n in dom (Opers (U2,B)) ; :: thesis: (Opers (U2,B)) . n = the charact of U0 . n
then reconsider o2 = the charact of U2 . n as operation of U2 by A30, FUNCT_1:def 3;
reconsider o21 = the charact of U1 . n as operation of U1 by A8, A30, A32, FUNCT_1:def 3;
A33: B2 is_closed_on o2 by A7;
A34: B1 is_closed_on o21 by A9;
thus (Opers (U2,B)) . n = o2 /. B by A32, Def6
.= o2 | ((arity o2) -tuples_on B) by A10, Def5
.= o2 | (((arity o2) -tuples_on B2) /\ ((arity o2) -tuples_on B)) by A31, MARGREL1:21
.= (o2 | ((arity o2) -tuples_on B2)) | ((arity o2) -tuples_on B) by RELAT_1:71
.= (o2 /. B2) | ((arity o2) -tuples_on B) by A33, Def5
.= o21 | ((arity o2) -tuples_on B) by A4, A8, A30, A32, Def6
.= o21 | ((arity o21) -tuples_on B1) by A2, A5, A8, A30, A32, Th6
.= o21 /. B1 by A34, Def5
.= the charact of U0 . n by A6, A29, A8, A30, A32, Def6 ; :: thesis: verum

end;

hence the charact of U0 = Opers (U2,B) by A29, A8, A30, FINSEQ_1:13; :: thesis: B is opers_closed
thus B is opers_closed by A10; :: thesis: verum