theorem Th25: :: MSAFREE5:46

for S being non empty non void ManySortedSign
for X being non-empty ManySortedSet of the carrier of S
for o being OperSymbol of S
for p being Element of Args (o,(Free (S,X))) holds
( { (height t1) where t1 is Element of (Free (S,X)) : t1 in rng p } is natural-membered & { (height t1) where t1 is Element of (Free (S,X)) : t1 in rng p } is finite & union { (height t) where t is Element of (Free (S,X)) : t in rng p } is Nat )