theorem Th26: :: MSAFREE5:47

for n being Nat
for S being non empty non void ManySortedSign
for o being OperSymbol of S
for X being non-empty ManySortedSet of the carrier of S
for p being Element of Args (o,(Free (S,X))) st the_arity_of o <> {} & n = union { (height t1) where t1 is Element of (Free (S,X)) : t1 in rng p } holds
height (o -term p) = n + 1