:: deftheorem Def9 defines PTDenOp OSAFREE:def 9 :
for S being OrderSortedSign
for X being non-empty ManySortedSet of S
for o being OperSymbol of S
for b₄ being Function of ((((ParsedTerms X) #) * the Arity of S) . o),(((ParsedTerms X) * the ResultSort of S) . o) holds
( b₄ = PTDenOp (o,X) iff for p being FinSequence of TS (DTConOSA X) st OSSym (o,X) ==> roots p holds
b₄ . p = (OSSym (o,X)) -tree p );