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 U0proof
let a be
set ;
:: according to TARSKI:def 3 :: thesis: ( not a in Constants U0 or a in Constants U1 )
assume A1:
a in Constants U0
;
:: thesis: a in Constants U1
then consider u being
Element of
U0 such that A2:
(
u = a & ex
o being
operation of
U0 st
(
arity o = 0 &
u in rng o ) )
;
consider o1 being
operation of
U0 such that A3:
(
arity o1 = 0 &
u in rng o1 )
by A2;
Constants U0 is
Subset of
U1
by UNIALG_2:18;
then consider u1 being
Element of
U1 such that A4:
u1 = u
by A1, A2;
consider x being
set such that A5:
(
x in dom the
charact of
U0 &
o1 = the
charact of
U0 . x )
by FUNCT_1:def 5;
reconsider x =
x as
Element of
NAT by A5;
reconsider A = the
carrier of
U1 as non
empty Subset of
U0 by UNIALG_2:def 8;
x in dom the
charact of
U1
by A5, UNIALG_2:10;
then reconsider o = the
charact of
U1 . x as
operation of
U1 by FUNCT_1:def 5;
x in dom (Opers U0,A)
by A5, UNIALG_2:def 7;
then A6:
(Opers U0,A) . x = o1 /. A
by A5, UNIALG_2:def 7;
A is
opers_closed
by UNIALG_2:def 8;
then A7:
A is_closed_on o1
by UNIALG_2:def 5;
A8:
dom o1 =
0 -tuples_on the
carrier of
U0
by A3, UNIALG_2:2
.=
{(<*> the carrier of U0)}
by FINSEQ_2:112
.=
{(<*> A)}
.=
0 -tuples_on A
by FINSEQ_2:112
;
o =
o1 /. A
by A6, UNIALG_2:def 8
.=
o1 | (0 -tuples_on A)
by A3, A7, UNIALG_2:def 6
.=
o1
by A8, RELAT_1:98
;
hence
a in Constants U1
by A2, A3, A4;
:: thesis: verum
end;
thus
Constants U1 c= Constants U0
:: thesis: verumproof
let a be
set ;
:: 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 A9:
(
u = a & ex
o being
operation of
U1 st
(
arity o = 0 &
u in rng o ) )
;
consider o being
operation of
U1 such that A10:
(
arity o = 0 &
u in rng o )
by A9;
the
carrier of
U1 is
Subset of
U0
by UNIALG_2:def 8;
then
u in the
carrier of
U0
by TARSKI:def 3;
then consider u1 being
Element of
U0 such that A11:
u1 = u
;
consider x being
set such that A12:
(
x in dom the
charact of
U1 &
o = the
charact of
U1 . x )
by FUNCT_1:def 5;
reconsider x =
x as
Element of
NAT by A12;
reconsider A = the
carrier of
U1 as non
empty Subset of
U0 by UNIALG_2:def 8;
A13:
x in dom the
charact of
U0
by A12, UNIALG_2:10;
then reconsider o1 = the
charact of
U0 . x as
operation of
U0 by FUNCT_1:def 5;
x in dom (Opers U0,A)
by A13, UNIALG_2:def 7;
then A14:
(Opers U0,A) . x = o1 /. A
by UNIALG_2:def 7;
A is
opers_closed
by UNIALG_2:def 8;
then A15:
A is_closed_on o1
by UNIALG_2:def 5;
len (signature U1) = len the
charact of
U1
by UNIALG_1:def 11;
then A16:
x in dom (signature U1)
by A12, FINSEQ_3:31;
U1,
U0 are_similar
by UNIALG_2:16;
then
signature U0 = signature U1
by UNIALG_2:def 2;
then A17:
arity o1 =
(signature U1) . x
by A16, UNIALG_1:def 11
.=
0
by A10, A12, A16, UNIALG_1:def 11
;
then A18:
dom o1 =
0 -tuples_on the
carrier of
U0
by UNIALG_2:2
.=
{(<*> the carrier of U0)}
by FINSEQ_2:112
.=
{(<*> A)}
.=
0 -tuples_on A
by FINSEQ_2:112
;
o =
o1 /. A
by A12, A14, UNIALG_2:def 8
.=
o1 | (0 -tuples_on A)
by A15, A17, UNIALG_2:def 6
.=
o1
by A18, RELAT_1:98
;
hence
a in Constants U0
by A9, A10, A11;
:: thesis: verum
end;