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