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