for S being non empty non void ManySortedSign
for X being V2() ManySortedSet of the carrier of S
for A being b₂,b₁ -terms all_vars_including vf-free VarMSAlgebra over S
for s being SortSymbol of S
for x being Element of A,s st x in (FreeGen X) . s holds
vf x = s -singleton x