for S being non empty non void ManySortedSign
for o being OperSymbol of S
for i being Element of NAT st i in dom (the_arity_of o) holds
for A1, A2 being MSAlgebra over S
for h being ManySortedFunction of A1,A2
for a, b being Element of Args (o,A1) st a in Args (o,A1) & h # a in Args (o,A2) holds
for f, g1, g2 being Function st f = a & g1 = h # a & g2 = h # b holds
for x being Element of A1,((the_arity_of o) /. i) st b = f +* (i,x) holds
( g2 . i = (h . ((the_arity_of o) /. i)) . x & h # b = g1 +* (i,(g2 . i)) )