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:10;
A4:
( len (FreeOpSeqZAO (f,D)) = len f & dom (FreeOpSeqZAO (f,D)) = Seg (len (FreeOpSeqZAO (f,D))) )
by Def17, FINSEQ_1:def 3;
then
the charact of (FreeUnivAlgZAO (f,D)) . n = FreeOpZAO (n,f,D)
by A2, A1, Def17;
then reconsider o = FreeOpZAO (n,f,D) as operation of (FreeUnivAlgZAO (f,D)) by A2, A4, A1, FUNCT_1:def 3;
A5:
( f /. n = f . n & dom (FreeOpZAO (n,f,D)) = (f /. n) -tuples_on (TS (DTConUA (f,D))) )
by A2, Def16, PARTFUN1:def 6;
then
dom o = {(<*> (TS (DTConUA (f,D))))}
by A3, FINSEQ_2:94;
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 3;
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 MARGREL1:22;
then
arity o = 0
by A3, A5, FINSEQ_2:110;
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