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

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

hence
Constants U0 is Subset of U1
; :: thesis: verum
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 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; :: thesis: verum

end;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 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; :: thesis: verum