consider o being operation of U0 such that

A1: arity o = 0 by Def11;

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

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

then <*> the carrier of U0 in dom o by TARSKI:def 1;

then A2: o . (<*> the carrier of U0) in rng o by FUNCT_1:def 3;

rng o c= the carrier of U0 by RELAT_1:def 19;

then reconsider u = o . (<*> the carrier of U0) as Element of U0 by A2;

u in { a where a is Element of U0 : ex o being operation of U0 st

( arity o = 0 & a in rng o ) } by A1, A2;

hence not Constants U0 is empty ; :: thesis: verum

A1: arity o = 0 by Def11;

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

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

then <*> the carrier of U0 in dom o by TARSKI:def 1;

then A2: o . (<*> the carrier of U0) in rng o by FUNCT_1:def 3;

rng o c= the carrier of U0 by RELAT_1:def 19;

then reconsider u = o . (<*> the carrier of U0) as Element of U0 by A2;

u in { a where a is Element of U0 : ex o being operation of U0 st

( arity o = 0 & a in rng o ) } by A1, A2;

hence not Constants U0 is empty ; :: thesis: verum