:: deftheorem Def10 defines PTOper OSAFREE:def 10 :
for S being OrderSortedSign
for X being non-empty ManySortedSet of S
for b₃ being ManySortedFunction of ((ParsedTerms X) #) * the Arity of S,(ParsedTerms X) * the ResultSort of S holds
( b₃ = PTOper X iff for o being OperSymbol of S holds b₃ . o = PTDenOp (o,X) );