let f be non empty with_zero FinSequence of NAT ; :: thesis: for D being disjoint_with_NAT set holds FreeUnivAlgZAO f,D is with_const_op
let D be disjoint_with_NAT set ; :: thesis: FreeUnivAlgZAO f,D is with_const_op
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;
take o ; :: according to UNIALG_2:def 12 :: thesis: arity o = 0
( 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;
hence arity o = 0 by A1, PRALG_1:1; :: thesis: verum