let U0 be Universal_Algebra; :: thesis: for U1, U2 being SubAlgebra of U0 st the carrier of U1 c= the carrier of U2 holds

U1 is SubAlgebra of U2

let U1, U2 be SubAlgebra of U0; :: thesis: ( the carrier of U1 c= the carrier of U2 implies U1 is SubAlgebra of U2 )

A1: dom the charact of U1 = dom the charact of U0 by Th7;

reconsider B1 = the carrier of U1 as non empty Subset of U0 by Def7;

assume A2: the carrier of U1 c= the carrier of U2 ; :: thesis: U1 is SubAlgebra of U2

hence the carrier of U1 is Subset of U2 ; :: according to UNIALG_2:def 7 :: thesis: for B being non empty Subset of U2 st B = the carrier of U1 holds

( the charact of U1 = Opers (U2,B) & B is opers_closed )

let B be non empty Subset of U2; :: thesis: ( B = the carrier of U1 implies ( the charact of U1 = Opers (U2,B) & B is opers_closed ) )

assume A3: B = the carrier of U1 ; :: thesis: ( the charact of U1 = Opers (U2,B) & B is opers_closed )

reconsider B2 = the carrier of U2 as non empty Subset of U0 by Def7;

A4: the charact of U2 = Opers (U0,B2) by Def7;

A5: B2 is opers_closed by Def7;

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

A7: dom the charact of U2 = dom the charact of U0 by Th7;

A8: B1 is opers_closed by Def7;

A9: B is opers_closed

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

U1 is SubAlgebra of U2

let U1, U2 be SubAlgebra of U0; :: thesis: ( the carrier of U1 c= the carrier of U2 implies U1 is SubAlgebra of U2 )

A1: dom the charact of U1 = dom the charact of U0 by Th7;

reconsider B1 = the carrier of U1 as non empty Subset of U0 by Def7;

assume A2: the carrier of U1 c= the carrier of U2 ; :: thesis: U1 is SubAlgebra of U2

hence the carrier of U1 is Subset of U2 ; :: according to UNIALG_2:def 7 :: thesis: for B being non empty Subset of U2 st B = the carrier of U1 holds

( the charact of U1 = Opers (U2,B) & B is opers_closed )

let B be non empty Subset of U2; :: thesis: ( B = the carrier of U1 implies ( the charact of U1 = Opers (U2,B) & B is opers_closed ) )

assume A3: B = the carrier of U1 ; :: thesis: ( the charact of U1 = Opers (U2,B) & B is opers_closed )

reconsider B2 = the carrier of U2 as non empty Subset of U0 by Def7;

A4: the charact of U2 = Opers (U0,B2) by Def7;

A5: B2 is opers_closed by Def7;

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

A7: dom the charact of U2 = dom the charact of U0 by Th7;

A8: B1 is opers_closed by Def7;

A9: B is opers_closed

proof

A17:
the charact of U1 = Opers (U0,B1)
by Def7;
let o2 be operation of U2; :: according to UNIALG_2:def 4 :: thesis: B is_closed_on o2

let s be FinSequence of B; :: according to UNIALG_2:def 3 :: thesis: ( len s = arity o2 implies o2 . s in B )

consider n being Nat such that

A10: n in dom the charact of U2 and

A11: the charact of U2 . n = o2 by FINSEQ_2:10;

reconsider o0 = the charact of U0 . n as operation of U0 by A7, A10, FUNCT_1:def 3;

A12: arity o2 = arity o0 by A10, A11, Th6;

rng s c= B by FINSEQ_1:def 4;

then rng s c= B2 by 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;

reconsider s1 = s as Element of B1 * by A3, FINSEQ_1:def 11;

assume A13: arity o2 = len s ; :: thesis: o2 . s in B

set tb2 = (arity o0) -tuples_on B2;

A14: B2 is_closed_on o0 by A5;

A15: o2 = o0 /. B2 by A4, A10, A11, Def6

.= o0 | ((arity o0) -tuples_on B2) by A14, Def5 ;

A16: B1 is_closed_on o0 by A8;

(arity o0) -tuples_on B2 = { w where w is Element of B2 * : len w = arity o0 } by FINSEQ_2:def 4;

then s2 in (arity o0) -tuples_on B2 by A13, A12;

then o2 . s = o0 . s1 by A15, FUNCT_1:49;

hence o2 . s in B by A3, A13, A16, A12; :: thesis: verum

end;let s be FinSequence of B; :: according to UNIALG_2:def 3 :: thesis: ( len s = arity o2 implies o2 . s in B )

consider n being Nat such that

A10: n in dom the charact of U2 and

A11: the charact of U2 . n = o2 by FINSEQ_2:10;

reconsider o0 = the charact of U0 . n as operation of U0 by A7, A10, FUNCT_1:def 3;

A12: arity o2 = arity o0 by A10, A11, Th6;

rng s c= B by FINSEQ_1:def 4;

then rng s c= B2 by 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;

reconsider s1 = s as Element of B1 * by A3, FINSEQ_1:def 11;

assume A13: arity o2 = len s ; :: thesis: o2 . s in B

set tb2 = (arity o0) -tuples_on B2;

A14: B2 is_closed_on o0 by A5;

A15: o2 = o0 /. B2 by A4, A10, A11, Def6

.= o0 | ((arity o0) -tuples_on B2) by A14, Def5 ;

A16: B1 is_closed_on o0 by A8;

(arity o0) -tuples_on B2 = { w where w is Element of B2 * : len w = arity o0 } by FINSEQ_2:def 4;

then s2 in (arity o0) -tuples_on B2 by A13, A12;

then o2 . s = o0 . s1 by A15, FUNCT_1:49;

hence o2 . s in B by A3, A13, A16, A12; :: thesis: verum

now :: thesis: for n being Nat st n in dom the charact of U0 holds

the charact of U1 . n = (Opers (U2,B)) . n

hence
the charact of U1 = Opers (U2,B)
by A1, A7, A6, FINSEQ_1:13; :: thesis: B is opers_closed the charact of U1 . n = (Opers (U2,B)) . n

let n be Nat; :: thesis: ( n in dom the charact of U0 implies the charact of U1 . n = (Opers (U2,B)) . n )

assume A18: n in dom the charact of U0 ; :: thesis: the charact of U1 . n = (Opers (U2,B)) . n

then reconsider o0 = the charact of U0 . n as operation of U0 by FUNCT_1:def 3;

reconsider o2 = the charact of U2 . n as operation of U2 by A7, A18, FUNCT_1:def 3;

A19: ( o2 = o0 /. B2 & arity o2 = arity o0 ) by A4, A7, A18, Def6, Th6;

A20: B is_closed_on o2 by A9;

A21: B2 is_closed_on o0 by A5;

A22: B1 is_closed_on o0 by A8;

thus the charact of U1 . n = o0 /. B1 by A17, A1, A18, Def6

.= o0 | ((arity o0) -tuples_on B1) by A22, Def5

.= o0 | (((arity o0) -tuples_on B2) /\ ((arity o0) -tuples_on B1)) by A2, MARGREL1:21

.= (o0 | ((arity o0) -tuples_on B2)) | ((arity o0) -tuples_on B) by A3, RELAT_1:71

.= (o0 /. B2) | ((arity o0) -tuples_on B) by A21, Def5

.= o2 /. B by A20, A19, Def5

.= (Opers (U2,B)) . n by A7, A6, A18, Def6 ; :: thesis: verum

end;assume A18: n in dom the charact of U0 ; :: thesis: the charact of U1 . n = (Opers (U2,B)) . n

then reconsider o0 = the charact of U0 . n as operation of U0 by FUNCT_1:def 3;

reconsider o2 = the charact of U2 . n as operation of U2 by A7, A18, FUNCT_1:def 3;

A19: ( o2 = o0 /. B2 & arity o2 = arity o0 ) by A4, A7, A18, Def6, Th6;

A20: B is_closed_on o2 by A9;

A21: B2 is_closed_on o0 by A5;

A22: B1 is_closed_on o0 by A8;

thus the charact of U1 . n = o0 /. B1 by A17, A1, A18, Def6

.= o0 | ((arity o0) -tuples_on B1) by A22, Def5

.= o0 | (((arity o0) -tuples_on B2) /\ ((arity o0) -tuples_on B1)) by A2, MARGREL1:21

.= (o0 | ((arity o0) -tuples_on B2)) | ((arity o0) -tuples_on B) by A3, RELAT_1:71

.= (o0 /. B2) | ((arity o0) -tuples_on B) by A21, Def5

.= o2 /. B by A20, A19, Def5

.= (Opers (U2,B)) . n by A7, A6, A18, Def6 ; :: thesis: verum

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