let U0 be Universal_Algebra; :: thesis: Constants U0 = { (o . {}) where o is operation of U0 : arity o = 0 }

set S = { (o . {}) where o is operation of U0 : arity o = 0 } ;

thus Constants U0 c= { (o . {}) where o is operation of U0 : arity o = 0 } :: according to XBOOLE_0:def 10 :: thesis: { (o . {}) where o is operation of U0 : arity o = 0 } c= Constants U0

set S = { (o . {}) where o is operation of U0 : arity o = 0 } ;

thus Constants U0 c= { (o . {}) where o is operation of U0 : arity o = 0 } :: according to XBOOLE_0:def 10 :: thesis: { (o . {}) where o is operation of U0 : arity o = 0 } c= Constants U0

proof

thus
{ (o . {}) where o is operation of U0 : arity o = 0 } c= Constants U0
:: thesis: verum
let a be object ; :: according to TARSKI:def 3 :: thesis: ( not a in Constants U0 or a in { (o . {}) where o is operation of U0 : arity o = 0 } )

assume a in Constants U0 ; :: thesis: a in { (o . {}) where o is operation of U0 : arity o = 0 }

then consider u being Element of U0 such that

A1: u = a and

A2: ex o being operation of U0 st

( arity o = 0 & u in rng o ) ;

consider o being operation of U0 such that

A3: arity o = 0 and

A4: u in rng o by A2;

consider a2 being object such that

A5: a2 in dom o and

A6: u = o . a2 by A4, FUNCT_1:def 3;

dom o = 0 -tuples_on the carrier of U0 by A3, MARGREL1:22;

then a2 is Tuple of 0 , the carrier of U0 by A5, FINSEQ_2:131;

then reconsider a1 = a2 as FinSequence of the carrier of U0 ;

len a1 = 0 by A3, A5, MARGREL1:def 25;

then a1 = {} ;

hence a in { (o . {}) where o is operation of U0 : arity o = 0 } by A1, A3, A6; :: thesis: verum

end;assume a in Constants U0 ; :: thesis: a in { (o . {}) where o is operation of U0 : arity o = 0 }

then consider u being Element of U0 such that

A1: u = a and

A2: ex o being operation of U0 st

( arity o = 0 & u in rng o ) ;

consider o being operation of U0 such that

A3: arity o = 0 and

A4: u in rng o by A2;

consider a2 being object such that

A5: a2 in dom o and

A6: u = o . a2 by A4, FUNCT_1:def 3;

dom o = 0 -tuples_on the carrier of U0 by A3, MARGREL1:22;

then a2 is Tuple of 0 , the carrier of U0 by A5, FINSEQ_2:131;

then reconsider a1 = a2 as FinSequence of the carrier of U0 ;

len a1 = 0 by A3, A5, MARGREL1:def 25;

then a1 = {} ;

hence a in { (o . {}) where o is operation of U0 : arity o = 0 } by A1, A3, A6; :: thesis: verum

proof

let a be object ; :: according to TARSKI:def 3 :: thesis: ( not a in { (o . {}) where o is operation of U0 : arity o = 0 } or a in Constants U0 )

assume a in { (o . {}) where o is operation of U0 : arity o = 0 } ; :: thesis: a in Constants U0

then consider o being operation of U0 such that

A7: a = o . {} and

A8: arity o = 0 ;

dom o = 0 -tuples_on the carrier of U0 by A8, MARGREL1:22

.= {(<*> the carrier of U0)} by FINSEQ_2:94 ;

then {} the carrier of U0 in dom o by TARSKI:def 1;

then o . ({} the carrier of U0) in rng o by FUNCT_1:def 3;

hence a in Constants U0 by A7, A8; :: thesis: verum

end;assume a in { (o . {}) where o is operation of U0 : arity o = 0 } ; :: thesis: a in Constants U0

then consider o being operation of U0 such that

A7: a = o . {} and

A8: arity o = 0 ;

dom o = 0 -tuples_on the carrier of U0 by A8, MARGREL1:22

.= {(<*> the carrier of U0)} by FINSEQ_2:94 ;

then {} the carrier of U0 in dom o by TARSKI:def 1;

then o . ({} the carrier of U0) in rng o by FUNCT_1:def 3;

hence a in Constants U0 by A7, A8; :: thesis: verum