:: deftheorem Def19 defines pi MSAFREE:def 19 :
for S being non empty non void ManySortedSign
for X, A being non-empty ManySortedSet of the carrier of S
for F being ManySortedFunction of FreeGen X,A
for t being Symbol of (DTConMSA X) st t in Terminals (DTConMSA 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) );