let f be non empty with_zero FinSequence of NAT ; for D being disjoint_with_NAT set holds FreeUnivAlgZAO f,D is with_const_op
let D be disjoint_with_NAT set ; FreeUnivAlgZAO f,D is with_const_op
set A = DTConUA f,D;
set AA = FreeUnivAlgZAO f,D;
A1:
dom f = Seg (len f)
by FINSEQ_1:def 3;
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;
take
o
; UNIALG_2:def 12 arity o = 0
A5:
dom o = (arity o) -tuples_on the carrier of (FreeUnivAlgZAO f,D)
by UNIALG_2:2;
( f /. n = f . n & dom (FreeOpZAO n,f,D) = (f /. n) -tuples_on (TS (DTConUA f,D)) )
by A2, Def17, PARTFUN1:def 8;
hence
arity o = 0
by A3, A5, FINSEQ_2:130; verum