let U0 be with_const_op Universal_Algebra; for U1 being SubAlgebra of U0 holds Constants U0 = Constants U1
let U1 be SubAlgebra of U0; Constants U0 = Constants U1
thus
Constants U0 c= Constants U1
XBOOLE_0:def 10 Constants U1 c= Constants U0proof
reconsider A = the
carrier of
U1 as non
empty Subset of
U0 by UNIALG_2:def 7;
let a be
object ;
TARSKI:def 3 ( 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
;
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;
verum
end;
thus
Constants U1 c= Constants U0
verumproof
reconsider A = the
carrier of
U1 as non
empty Subset of
U0 by UNIALG_2:def 7;
let a be
object ;
TARSKI:def 3 ( not a in Constants U1 or a in Constants U0 )
assume
a in Constants U1
;
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;
verum
end;