:: deftheorem Def13 defines FreeOper MSAFREE:def 13 :
for S being non empty non void ManySortedSign
for X being non-empty ManySortedSet of the carrier of S
for b₃ being ManySortedFunction of ((FreeSort X) #) * the Arity of S,(FreeSort X) * the ResultSort of S holds
( b₃ = FreeOper X iff for o being OperSymbol of S holds b₃ . o = DenOp (o,X) );