let S be 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 s2,s3 holds
for f being Function st f is_e.translation_of A,s1,s2 holds
for t being Translation of A,s2,s3 holds t * f is Translation of A,s1,s3
let A be non-empty MSAlgebra over S; for s1, s2, s3 being SortSymbol of S st TranslationRel S reduces s2,s3 holds
for f being Function st f is_e.translation_of A,s1,s2 holds
for t being Translation of A,s2,s3 holds t * f is Translation of A,s1,s3
let s1, s2, s3 be SortSymbol of S; ( TranslationRel S reduces s2,s3 implies for f being Function st f is_e.translation_of A,s1,s2 holds
for t being Translation of A,s2,s3 holds t * f is Translation of A,s1,s3 )
assume A1:
TranslationRel S reduces s2,s3
; for f being Function st f is_e.translation_of A,s1,s2 holds
for t being Translation of A,s2,s3 holds t * f is Translation of A,s1,s3
let f be Function; ( f is_e.translation_of A,s1,s2 implies for t being Translation of A,s2,s3 holds t * f is Translation of A,s1,s3 )
assume A2:
f is_e.translation_of A,s1,s2
; for t being Translation of A,s2,s3 holds t * f is Translation of A,s1,s3
then A3:
f is Translation of A,s1,s2
by Th17;
TranslationRel S reduces s1,s2
by A2, Th17;
hence
for t being Translation of A,s2,s3 holds t * f is Translation of A,s1,s3
by A1, A3, Th18; verum