let f be non empty with_zero FinSequence of NAT ; :: thesis: for D being disjoint_with_NAT set holds Constants (FreeUnivAlgZAO f,D) <> {}
let D be disjoint_with_NAT set ; :: thesis: Constants (FreeUnivAlgZAO f,D) <> {}
set A = DTConUA f,D;
set AA = FreeUnivAlgZAO f,D;
0 in rng f by Def2;
then consider n being Nat such that
A1: ( n in dom f & f . n = 0 ) by FINSEQ_2:11;
A2: len (FreeOpSeqZAO f,D) = len f by Def18;
A3: ( dom (FreeOpSeqZAO f,D) = Seg (len (FreeOpSeqZAO f,D)) & dom f = Seg (len f) ) by FINSEQ_1:def 3;
then the charact of (FreeUnivAlgZAO f,D) . n = FreeOpZAO n,f,D by A1, A2, Def18;
then reconsider o = FreeOpZAO n,f,D as operation of (FreeUnivAlgZAO f,D) by A1, A2, A3, FUNCT_1:def 5;
set ca = the carrier of (FreeUnivAlgZAO f,D);
A4: ( dom o = (arity o) -tuples_on the carrier of (FreeUnivAlgZAO f,D) & f /. n = f . n & dom (FreeOpZAO n,f,D) = (f /. n) -tuples_on (TS (DTConUA f,D)) ) by A1, Def17, PARTFUN1:def 8, UNIALG_2:2;
then A5: arity o = 0 by A1, PRALG_1:1;
dom o = {(<*> (TS (DTConUA f,D)))} by A1, A4, FINSEQ_2:112;
then <*> (TS (DTConUA f,D)) in dom o by TARSKI:def 1;
then A6: ( o . (<*> (TS (DTConUA f,D))) in rng o & rng o c= the carrier of (FreeUnivAlgZAO f,D) ) by FUNCT_1:def 5, RELSET_1:12;
then reconsider e = o . (<*> (TS (DTConUA f,D))) as Element of the carrier of (FreeUnivAlgZAO f,D) ;
e in { a where a is Element of the carrier of (FreeUnivAlgZAO f,D) : ex o being operation of (FreeUnivAlgZAO f,D) st
( arity o = 0 & a in rng o ) } by A5, A6;
hence Constants (FreeUnivAlgZAO f,D) <> {} ; :: thesis: verum