:: deftheorem defines growable MSAFREE5:def 5 :
for S being non empty non void ManySortedSign holds
( S is growable iff for X being V5() ManySortedSet of the carrier of S
for n being Nat ex t being Element of (Free (S,X)) st height (dom t) = n );