:: deftheorem Def17 defines FreeOpSeqZAO FREEALG:def 17 :
for f being non empty with_zero FinSequence of NAT
for D being disjoint_with_NAT set
for b₃ being PFuncFinSequence of (TS (DTConUA (f,D))) holds
( b₃ = FreeOpSeqZAO (f,D) iff ( len b₃ = len f & ( for n being Nat st n in dom b₃ holds
b₃ . n = FreeOpZAO (n,f,D) ) ) );