:: deftheorem defines substitution ABCMIZ_1:def 57 :
for S being non void Signature
for X being ManySortedSet of the carrier of S
for t being term-transformation of S,X holds
( t is substitution iff for o being OperSymbol of S
for p, q being FinSequence of (Free (S,X)) st [o, the carrier of S] -tree p in Union the Sorts of (Free (S,X)) & q = t * p holds
t . ([o, the carrier of S] -tree p) = [o, the carrier of S] -tree q );