for S being non empty non void ManySortedSign
for X being V5() ManySortedSet of S
for A0 being non-empty b₂,b₁ -terms MSAlgebra over S
for t being Element of A0
for s being SortSymbol of S st t in the Sorts of (Free (S,X)) . s holds
t in the Sorts of A0 . s