theorem :: MSAFREE5:60

for i being Nat
for S being non empty non void ManySortedSign
for X being non-empty ManySortedSet of the carrier of S
for T being b₃,b₂ -terms all_vars_including inheriting_operations free_in_itself MSAlgebra over S holds T deg<= (i + 1) = (T deg<= 0) \/ ( { (o -term p) where o is OperSymbol of S, p is Element of Args (o,(Free (S,X))) : ex f being FinSequence of NAT st
( i >= Sum f & dom f = dom (the_arity_of o) & ( for i being Nat
for t being Element of (Free (S,X)) st i in dom (the_arity_of o) & t = p . i holds
f . i = deg t ) ) } /\ (Union the Sorts of T))