:: deftheorem Def15 defines # MSAFREE4:def 15 :
for S being non empty non void ManySortedSign
for X being non-empty ManySortedSet of S
for w being ManySortedFunction of X, the carrier of S --> NAT
for t being Function st t is Element of (Free (S,X)) holds
for b₅ being Element of (TermAlg S) holds
( b₅ = # (t,w) iff ex F being ManySortedSet of S -Terms X st
( b₅ = F . t & ( for s being SortSymbol of S
for x being Element of X . s holds F . (root-tree [x,s]) = root-tree [((w . s) . x),s] ) & ( for o being OperSymbol of S
for p being ArgumentSeq of Sym (o,X) holds F . ((Sym (o,X)) -tree p) = (Sym (o,( the carrier of S --> NAT))) -tree (F * p) ) ) );