:: deftheorem Def56 defines term-transformation ABCMIZ_1:def 56 :
for S being non void Signature
for X being ManySortedSet of the carrier of S
for b₃ being UnOp of (Union the Sorts of (Free (S,X))) holds
( b₃ is term-transformation of S,X iff for s being SortSymbol of S holds b₃ .: ( the Sorts of (Free (S,X)) . s) c= the Sorts of (Free (S,X)) . s );