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