let U0 be with_const_op Universal_Algebra; :: thesis: for U1 being SubAlgebra of U0 holds Constants U0 = Constants U1

let U1 be SubAlgebra of U0; :: thesis: Constants U0 = Constants U1

thus Constants U0 c= Constants U1 :: according to XBOOLE_0:def 10 :: thesis: Constants U1 c= Constants U0

let U1 be SubAlgebra of U0; :: thesis: Constants U0 = Constants U1

thus Constants U0 c= Constants U1 :: according to XBOOLE_0:def 10 :: thesis: Constants U1 c= Constants U0

proof

thus
Constants U1 c= Constants U0
:: thesis: verum
reconsider A = the carrier of U1 as non empty Subset of U0 by UNIALG_2:def 7;

let a be object ; :: according to TARSKI:def 3 :: thesis: ( not a in Constants U0 or a in Constants U1 )

A1: Constants U0 is Subset of U1 by UNIALG_2:15;

assume A2: a in Constants U0 ; :: thesis: a in Constants U1

then consider u being Element of U0 such that

A3: u = a and

A4: ex o being operation of U0 st

( arity o = 0 & u in rng o ) ;

consider o1 being operation of U0 such that

A5: arity o1 = 0 and

A6: u in rng o1 by A4;

A7: dom o1 = 0 -tuples_on the carrier of U0 by A5, MARGREL1:22

.= {(<*> the carrier of U0)} by FINSEQ_2:94

.= {(<*> A)}

.= 0 -tuples_on A by FINSEQ_2:94 ;

consider x being object such that

A8: x in dom the charact of U0 and

A9: o1 = the charact of U0 . x by FUNCT_1:def 3;

reconsider x = x as Element of NAT by A8;

x in dom the charact of U1 by A8, UNIALG_2:7;

then reconsider o = the charact of U1 . x as operation of U1 by FUNCT_1:def 3;

A is opers_closed by UNIALG_2:def 7;

then A10: A is_closed_on o1 ;

x in dom (Opers (U0,A)) by A8, UNIALG_2:def 6;

then (Opers (U0,A)) . x = o1 /. A by A9, UNIALG_2:def 6;

then o = o1 /. A by UNIALG_2:def 7

.= o1 | (0 -tuples_on A) by A5, A10, UNIALG_2:def 5

.= o1 by A7, RELAT_1:69 ;

hence a in Constants U1 by A2, A3, A5, A6, A1; :: thesis: verum

end;let a be object ; :: according to TARSKI:def 3 :: thesis: ( not a in Constants U0 or a in Constants U1 )

A1: Constants U0 is Subset of U1 by UNIALG_2:15;

assume A2: a in Constants U0 ; :: thesis: a in Constants U1

then consider u being Element of U0 such that

A3: u = a and

A4: ex o being operation of U0 st

( arity o = 0 & u in rng o ) ;

consider o1 being operation of U0 such that

A5: arity o1 = 0 and

A6: u in rng o1 by A4;

A7: dom o1 = 0 -tuples_on the carrier of U0 by A5, MARGREL1:22

.= {(<*> the carrier of U0)} by FINSEQ_2:94

.= {(<*> A)}

.= 0 -tuples_on A by FINSEQ_2:94 ;

consider x being object such that

A8: x in dom the charact of U0 and

A9: o1 = the charact of U0 . x by FUNCT_1:def 3;

reconsider x = x as Element of NAT by A8;

x in dom the charact of U1 by A8, UNIALG_2:7;

then reconsider o = the charact of U1 . x as operation of U1 by FUNCT_1:def 3;

A is opers_closed by UNIALG_2:def 7;

then A10: A is_closed_on o1 ;

x in dom (Opers (U0,A)) by A8, UNIALG_2:def 6;

then (Opers (U0,A)) . x = o1 /. A by A9, UNIALG_2:def 6;

then o = o1 /. A by UNIALG_2:def 7

.= o1 | (0 -tuples_on A) by A5, A10, UNIALG_2:def 5

.= o1 by A7, RELAT_1:69 ;

hence a in Constants U1 by A2, A3, A5, A6, A1; :: thesis: verum

proof

reconsider A = the carrier of U1 as non empty Subset of U0 by UNIALG_2:def 7;

let a be object ; :: according to TARSKI:def 3 :: thesis: ( not a in Constants U1 or a in Constants U0 )

assume a in Constants U1 ; :: thesis: a in Constants U0

then consider u being Element of U1 such that

A11: u = a and

A12: ex o being operation of U1 st

( arity o = 0 & u in rng o ) ;

consider o being operation of U1 such that

A13: arity o = 0 and

A14: u in rng o by A12;

consider x being object such that

A15: x in dom the charact of U1 and

A16: o = the charact of U1 . x by FUNCT_1:def 3;

reconsider x = x as Element of NAT by A15;

A17: x in dom the charact of U0 by A15, UNIALG_2:7;

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

len (signature U1) = len the charact of U1 by UNIALG_1:def 4;

then A18: x in dom (signature U1) by A15, FINSEQ_3:29;

U1,U0 are_similar by UNIALG_2:13;

then signature U0 = signature U1 ;

then A19: arity o1 = (signature U1) . x by A18, UNIALG_1:def 4

.= 0 by A13, A16, A18, UNIALG_1:def 4 ;

then A20: dom o1 = 0 -tuples_on the carrier of U0 by MARGREL1:22

.= {(<*> the carrier of U0)} by FINSEQ_2:94

.= {(<*> A)}

.= 0 -tuples_on A by FINSEQ_2:94 ;

A is opers_closed by UNIALG_2:def 7;

then A21: A is_closed_on o1 ;

the carrier of U1 is Subset of U0 by UNIALG_2:def 7;

then A22: u in the carrier of U0 by TARSKI:def 3;

x in dom (Opers (U0,A)) by A17, UNIALG_2:def 6;

then (Opers (U0,A)) . x = o1 /. A by UNIALG_2:def 6;

then o = o1 /. A by A16, UNIALG_2:def 7

.= o1 | (0 -tuples_on A) by A21, A19, UNIALG_2:def 5

.= o1 by A20, RELAT_1:69 ;

hence a in Constants U0 by A11, A13, A14, A22; :: thesis: verum

end;let a be object ; :: according to TARSKI:def 3 :: thesis: ( not a in Constants U1 or a in Constants U0 )

assume a in Constants U1 ; :: thesis: a in Constants U0

then consider u being Element of U1 such that

A11: u = a and

A12: ex o being operation of U1 st

( arity o = 0 & u in rng o ) ;

consider o being operation of U1 such that

A13: arity o = 0 and

A14: u in rng o by A12;

consider x being object such that

A15: x in dom the charact of U1 and

A16: o = the charact of U1 . x by FUNCT_1:def 3;

reconsider x = x as Element of NAT by A15;

A17: x in dom the charact of U0 by A15, UNIALG_2:7;

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

len (signature U1) = len the charact of U1 by UNIALG_1:def 4;

then A18: x in dom (signature U1) by A15, FINSEQ_3:29;

U1,U0 are_similar by UNIALG_2:13;

then signature U0 = signature U1 ;

then A19: arity o1 = (signature U1) . x by A18, UNIALG_1:def 4

.= 0 by A13, A16, A18, UNIALG_1:def 4 ;

then A20: dom o1 = 0 -tuples_on the carrier of U0 by MARGREL1:22

.= {(<*> the carrier of U0)} by FINSEQ_2:94

.= {(<*> A)}

.= 0 -tuples_on A by FINSEQ_2:94 ;

A is opers_closed by UNIALG_2:def 7;

then A21: A is_closed_on o1 ;

the carrier of U1 is Subset of U0 by UNIALG_2:def 7;

then A22: u in the carrier of U0 by TARSKI:def 3;

x in dom (Opers (U0,A)) by A17, UNIALG_2:def 6;

then (Opers (U0,A)) . x = o1 /. A by UNIALG_2:def 6;

then o = o1 /. A by A16, UNIALG_2:def 7

.= o1 | (0 -tuples_on A) by A21, A19, UNIALG_2:def 5

.= o1 by A20, RELAT_1:69 ;

hence a in Constants U0 by A11, A13, A14, A22; :: thesis: verum