for S being non empty non void ManySortedSign
for A being non-empty MSAlgebra over S
for V being Variables of A
for f being ManySortedFunction of V, the Sorts of A
for s being SortSymbol of S
for x being Element of the Sorts of A . s holds (x -term (A,V)) @ f = x