:: deftheorem Def12 defines DenOp MSAFREE:def 12 :
for S being non empty non void ManySortedSign
for X being non-empty ManySortedSet of the carrier of S
for o being OperSymbol of S
for b₄ being Function of ((((FreeSort X) #) * the Arity of S) . o),(((FreeSort X) * the ResultSort of S) . o) holds
( b₄ = DenOp (o,X) iff for p being FinSequence of TS (DTConMSA X) st Sym (o,X) ==> roots p holds
b₄ . p = (Sym (o,X)) -tree p );