for i, j being Nat
for S being non empty non void ManySortedSign
for X being V5() ManySortedSet of the carrier of S
for T being b₄,b₃ -terms all_vars_including inheriting_operations free_in_itself MSAlgebra over S st i <= j holds
T height<= i c= T height<= j