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 ;
reconsider B2 = the carrier of U1 as non empty Subset of U2 by ;
A4: the charact of U1 = Opers (U2,B2) by ;
the carrier of U1 is Subset of U2 by ;
hence the carrier of U0 is Subset of U2 by ; :: 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 ;
A6: the charact of U0 = Opers (U1,B1) by ;
A7: B2 is opers_closed by ;
A8: dom the charact of U1 = dom (Opers (U2,B2)) by
.= dom the charact of U2 by Def6 ;
A9: B1 is opers_closed by ;
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 ;
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 ;
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 ;
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 ;
then A20: arity o2 = arity o21 by ;
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 ;
then (arity o20) -tuples_on B1 = ((arity o21) -tuples_on the carrier of U1) /\ ((arity o21) -tuples_on B1) by ;
then A23: arity o20 = arity o21 by ;
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 ;
reconsider s0 = s as Element of the carrier of U0 * by ;
A24: rng o20 c= B by ;
rng s c= B by FINSEQ_1:def 4;
then rng s c= B2 by ;
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 ;
then s0 in (arity o20) -tuples_on the carrier of U0 by FINSEQ_2:def 4;
then A27: o20 . s0 in rng o20 by ;
s1 in { w where w is Element of B1 * : len w = arity o21 } by ;
then A28: s1 in (arity o21) -tuples_on B1 by FINSEQ_2:def 4;
o20 . s0 = (o21 | ((arity o21) -tuples_on B1)) . s1 by
.= o21 . s1 by
.= (o2 | ((arity o2) -tuples_on B2)) . s2 by
.= o2 . s by ;
hence o2 . s in B by ; :: thesis: verum
end;
hence B is_closed_on o2 ; :: thesis: verum
end;
A29: dom the charact of U0 = dom (Opers (U1,B1)) by
.= 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 ;
reconsider o21 = the charact of U1 . n as operation of U1 by ;
A33: B2 is_closed_on o2 by A7;
A34: B1 is_closed_on o21 by A9;
thus (Opers (U2,B)) . n = o2 /. B by
.= o2 | ((arity o2) -tuples_on B) by
.= o2 | (((arity o2) -tuples_on B2) /\ ((arity o2) -tuples_on B)) by
.= (o2 | ((arity o2) -tuples_on B2)) | ((arity o2) -tuples_on B) by RELAT_1:71
.= (o2 /. B2) | ((arity o2) -tuples_on B) by
.= 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
.= the charact of U0 . n by A6, A29, A8, A30, A32, Def6 ; :: thesis: verum
end;
hence the charact of U0 = Opers (U2,B) by ; :: thesis: B is opers_closed
thus B is opers_closed by A10; :: thesis: verum