for S being non empty non void ManySortedSign
for X being V5() ManySortedSet of S
for A being b₂,b₁ -terms all_vars_including inheriting_operations free_in_itself MSAlgebra over S
for w being ManySortedFunction of the carrier of S --> NAT,X ex h being ManySortedFunction of (TermAlg S),A st
( h is_homomorphism TermAlg S,A & ( for s being SortSymbol of S
for i being Nat holds (h . s) . (root-tree [i,s]) = root-tree [((w . s) . i),s] ) )