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