:: deftheorem Def14 defines pi OSAFREE:def 14 :
for S being monotone regular locally_directed OrderSortedSign
for X being V2() ManySortedSet of S
for o being OperSymbol of S
for x being FinSequence of TS (DTConOSA X) st OSSym ((LBound (o,(LeastSorts x))),X) ==> roots x holds
pi (o,x) = (OSSym ((LBound (o,(LeastSorts x))),X)) -tree x;