for S being non empty non void ManySortedSign
for A being V2() ManySortedSet of the carrier of S
for f being ManySortedFunction of (A #) * the Arity of S,A * the ResultSort of S
for o being OperSymbol of S
for d being Function of (((A #) * the Arity of S) . o),((A * the ResultSort of S) . o) holds f +* (o,d) is ManySortedFunction of (A #) * the Arity of S,A * the ResultSort of S