:: deftheorem Def10 defines FreeOpNSG FREEALG:def 10 :
for f being non empty FinSequence of NAT
for D being non empty disjoint_with_NAT set
for n being Nat st n in dom f holds
for b₄ being non empty homogeneous quasi_total PartFunc of ((TS (DTConUA (f,D))) *),(TS (DTConUA (f,D))) holds
( b₄ = FreeOpNSG (n,f,D) iff ( dom b₄ = (f /. n) -tuples_on (TS (DTConUA (f,D))) & ( for p being FinSequence of TS (DTConUA (f,D)) st p in dom b₄ holds
b₄ . p = (Sym (n,f,D)) -tree p ) ) );