theorem Th5:
for
S being non
empty non
void ManySortedSign for
A1,
A2,
B1,
B2 being
MSAlgebra over
S st
MSAlgebra(# the
Sorts of
A1, the
Charact of
A1 #)
= MSAlgebra(# the
Sorts of
B1, the
Charact of
B1 #) &
MSAlgebra(# the
Sorts of
A2, the
Charact of
A2 #)
= MSAlgebra(# the
Sorts of
B2, the
Charact of
B2 #) holds
for
f being
ManySortedFunction of
A1,
A2 for
g being
ManySortedFunction of
B1,
B2 st
f = g holds
for
o being
OperSymbol of
S st
Args (
o,
A1)
<> {} &
Args (
o,
A2)
<> {} holds
for
x being
Element of
Args (
o,
A1)
for
y being
Element of
Args (
o,
B1) st
x = y holds
f # x = g # y