let U0 be Universal_Algebra; for U1 being SubAlgebra of U0 holds Constants U0 is Subset of U1
let U1 be SubAlgebra of U0; Constants U0 is Subset of U1
set u1 = the carrier of U1;
Constants U0 c= the carrier of U1
proof
reconsider B = the
carrier of
U1 as non
empty Subset of
U0 by Def7;
let x be
object ;
TARSKI:def 3 ( not x in Constants U0 or x in the carrier of U1 )
assume
x in Constants U0
;
x in the carrier of U1
then consider a being
Element of
U0 such that A1:
a = x
and A2:
ex
o being
operation of
U0 st
(
arity o = 0 &
a in rng o )
;
consider o0 being
operation of
U0 such that A3:
arity o0 = 0
and A4:
a in rng o0
by A2;
consider y being
object such that A5:
y in dom o0
and A6:
a = o0 . y
by A4, FUNCT_1:def 3;
dom o0 =
0 -tuples_on the
carrier of
U0
by A3, MARGREL1:22
.=
{(<*> the carrier of U0)}
by FINSEQ_2:94
;
then
y in {(<*> B)}
by A5;
then
y in 0 -tuples_on B
by FINSEQ_2:94;
then
y in (dom o0) /\ ((arity o0) -tuples_on B)
by A3, A5, XBOOLE_0:def 4;
then A7:
y in dom (o0 | ((arity o0) -tuples_on B))
by RELAT_1:61;
consider n being
Nat such that A8:
n in dom the
charact of
U0
and A9:
the
charact of
U0 . n = o0
by FINSEQ_2:10;
A10:
n in dom the
charact of
U1
by A8, Th7;
then reconsider o1 = the
charact of
U1 . n as
operation of
U1 by FUNCT_1:def 3;
the
charact of
U1 = Opers (
U0,
B)
by Def7;
then A11:
o1 = o0 /. B
by A9, A10, Def6;
B is
opers_closed
by Def7;
then A12:
B is_closed_on o0
;
then
y in dom (o0 /. B)
by A7, Def5;
then A13:
o1 . y in rng o1
by A11, FUNCT_1:def 3;
A14:
rng o1 c= the
carrier of
U1
by RELAT_1:def 19;
o1 . y =
(o0 | ((arity o0) -tuples_on B)) . y
by A11, A12, Def5
.=
a
by A6, A7, FUNCT_1:47
;
hence
x in the
carrier of
U1
by A1, A13, A14;
verum
end;
hence
Constants U0 is Subset of U1
; verum