let S be non empty non void ManySortedSign ; :: thesis: for A being non-empty MSAlgebra of S
for s1, s2, s3 being SortSymbol of S st TranslationRel S reduces s1,s2 holds
for t being Translation of A,s1,s2
for f being Function st f is_e.translation_of A,s2,s3 holds
f * t is Translation of A,s1,s3
let A be non-empty MSAlgebra of S; :: thesis: for s1, s2, s3 being SortSymbol of S st TranslationRel S reduces s1,s2 holds
for t being Translation of A,s1,s2
for f being Function st f is_e.translation_of A,s2,s3 holds
f * t is Translation of A,s1,s3
let s1, s2, s3 be SortSymbol of S; :: thesis: ( TranslationRel S reduces s1,s2 implies for t being Translation of A,s1,s2
for f being Function st f is_e.translation_of A,s2,s3 holds
f * t is Translation of A,s1,s3 )
assume A1: TranslationRel S reduces s1,s2 ; :: thesis: for t being Translation of A,s1,s2
for f being Function st f is_e.translation_of A,s2,s3 holds
f * t is Translation of A,s1,s3
let t be Translation of A,s1,s2; :: thesis: for f being Function st f is_e.translation_of A,s2,s3 holds
f * t is Translation of A,s1,s3
let f be Function; :: thesis: ( f is_e.translation_of A,s2,s3 implies f * t is Translation of A,s1,s3 )
assume f is_e.translation_of A,s2,s3 ; :: thesis: f * t is Translation of A,s1,s3
then ( TranslationRel S reduces s2,s3 & f is Translation of A,s2,s3 ) by Th17;
hence f * t is Translation of A,s1,s3 by A1, Th18; :: thesis: verum