:: deftheorem Def28 defines pi OSAFREE:def 28 :
for S being locally_directed OrderSortedSign
for X being V2() ManySortedSet of S
for A being V2() ManySortedSet of the carrier of S
for F being ManySortedFunction of PTVars X,A
for t being Symbol of (DTConOSA X) st t in Terminals (DTConOSA X) holds
for b₆ being Element of Union A holds
( b₆ = pi (F,A,t) iff for f being Function st f = F . (t `2) holds
b₆ = f . (root-tree t) );