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: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
; UNIALG_2:def 11 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; verum