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);
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: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;
take o ; :: according to UNIALG_2:def 11 :: thesis: arity o = 0
A5: dom o = (arity o) -tuples_on the carrier of (FreeUnivAlgZAO (f,D)) by MARGREL1:22;
( f /. n = f . n & dom (FreeOpZAO (n,f,D)) = (f /. n) -tuples_on (TS (DTConUA (f,D))) ) by A2, Def16, PARTFUN1:def 6;
hence arity o = 0 by A3, A5, FINSEQ_2:110; :: thesis: verum