for S being non empty non void ManySortedSign
for s being SortSymbol of S
for A being non-empty disjoint_valued MSAlgebra over S
for B being non-empty MSAlgebra over S
for f being ManySortedFunction of A,B
for a being Element of the Sorts of A . s holds f . a is Element of the Sorts of B . s