theorem Th9:
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)) )