:: deftheorem Def45 defines variables_in ABCMIZ_1:def 45 :
for S being non void Signature
for X being empty-yielding ManySortedSet of the carrier of S
for s being SortSymbol of S
for b₄ being Function of (Union the Sorts of (Free (S,X))),(bool (X . s)) holds
( b₄ = (X,s) variables_in iff for t being Element of (Free (S,X)) holds b₄ . t = (S variables_in t) . s );