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
reconsider B = the carrier of U1 as non empty Subset of U0 by Def7;
let x be object ; :: 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 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 ;
dom o0 = 0 -tuples_on the carrier of U0 by
.= {(<*> 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 ;
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 ;
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 ;
B is opers_closed by Def7;
then A12: B is_closed_on o0 ;
then y in dom (o0 /. B) by ;
then A13: o1 . y in rng o1 by ;
A14: rng o1 c= the carrier of U1 by RELAT_1:def 19;
o1 . y = (o0 | ((arity o0) -tuples_on B)) . y by
.= a by ;
hence x in the carrier of U1 by A1, A13, A14; :: thesis: verum
end;
hence Constants U0 is Subset of U1 ; :: thesis: verum