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;

.= dom the charact of U1 by Def6 ;

A30: dom the charact of U2 = dom (Opers (U2,B)) by Def6;

A31: B = B1 by A5;

thus B is opers_closed by A10; :: thesis: verum

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

A29: dom the charact of U0 =
dom (Opers (U1,B1))
by A1, Def7
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;

end;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

hence
B is_closed_on o2
; :: thesis: verumo2 . 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;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

.= 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

hence
the charact of U0 = Opers (U2,B)
by A29, A8, A30, FINSEQ_1:13; :: thesis: B is opers_closed (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;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

thus B is opers_closed by A10; :: thesis: verum