:: deftheorem Def9 defines Sym FREEALG:def 9 :
for f being non empty FinSequence of NAT
for X being set
for n being Nat st n in dom f holds
Sym (n,f,X) = n;