theorem Th18:
for
S being non
empty non
void ManySortedSign for
A being
non-empty MSAlgebra over
S for
s1,
s2,
s3 being
SortSymbol of
S st
TranslationRel S reduces s1,
s2 &
TranslationRel S reduces s2,
s3 holds
for
t1 being
Translation of
A,
s1,
s2 for
t2 being
Translation of
A,
s2,
s3 holds
t2 * t1 is
Translation of
A,
s1,
s3