for S being non empty non void ManySortedSign
for A being non-empty disjoint_valued MSAlgebra over S
for B being non-empty MSAlgebra over S
for o being OperSymbol of S
for p, q being Element of Args (o,A)
for h being ManySortedFunction of A,B
for a being Element of A
for i being Nat st i in dom p & q = p +* (i,a) holds
h # q = (h # p) +* (i,(h . a))