for S being non empty non void ManySortedSign
for X being V5() ManySortedSet of S
for A1 being b₂,b₁ -terms all_vars_including MSAlgebra over S
for s being SortSymbol of S
for x being Element of X . s holds root-tree [x,s] is Element of A1,s