let S, S' be non empty non void ManySortedSign ; :: thesis: for A being non-empty MSAlgebra of S
for f being Function of the carrier of S',the carrier of S
for g being Function st f,g form_morphism_between S',S holds
for B being non-empty MSAlgebra of S' st B = A | S',f,g holds
for s1, s2 being SortSymbol of S' st TranslationRel S' reduces s1,s2 holds
( TranslationRel S reduces f . s1,f . s2 & ( for t being Translation of B,s1,s2 holds t is Translation of A,f . s1,f . s2 ) )
let A be non-empty MSAlgebra of S; :: thesis: for f being Function of the carrier of S',the carrier of S
for g being Function st f,g form_morphism_between S',S holds
for B being non-empty MSAlgebra of S' st B = A | S',f,g holds
for s1, s2 being SortSymbol of S' st TranslationRel S' reduces s1,s2 holds
( TranslationRel S reduces f . s1,f . s2 & ( for t being Translation of B,s1,s2 holds t is Translation of A,f . s1,f . s2 ) )
let f be Function of the carrier of S',the carrier of S; :: thesis: for g being Function st f,g form_morphism_between S',S holds
for B being non-empty MSAlgebra of S' st B = A | S',f,g holds
for s1, s2 being SortSymbol of S' st TranslationRel S' reduces s1,s2 holds
( TranslationRel S reduces f . s1,f . s2 & ( for t being Translation of B,s1,s2 holds t is Translation of A,f . s1,f . s2 ) )
let g be Function; :: thesis: ( f,g form_morphism_between S',S implies for B being non-empty MSAlgebra of S' st B = A | S',f,g holds
for s1, s2 being SortSymbol of S' st TranslationRel S' reduces s1,s2 holds
( TranslationRel S reduces f . s1,f . s2 & ( for t being Translation of B,s1,s2 holds t is Translation of A,f . s1,f . s2 ) ) )
assume A1: f,g form_morphism_between S',S ; :: thesis: for B being non-empty MSAlgebra of S' st B = A | S',f,g holds
for s1, s2 being SortSymbol of S' st TranslationRel S' reduces s1,s2 holds
( TranslationRel S reduces f . s1,f . s2 & ( for t being Translation of B,s1,s2 holds t is Translation of A,f . s1,f . s2 ) )
let B be non-empty MSAlgebra of S'; :: thesis: ( B = A | S',f,g implies for s1, s2 being SortSymbol of S' st TranslationRel S' reduces s1,s2 holds
( TranslationRel S reduces f . s1,f . s2 & ( for t being Translation of B,s1,s2 holds t is Translation of A,f . s1,f . s2 ) ) )
assume A2: B = A | S',f,g ; :: thesis: for s1, s2 being SortSymbol of S' st TranslationRel S' reduces s1,s2 holds
( TranslationRel S reduces f . s1,f . s2 & ( for t being Translation of B,s1,s2 holds t is Translation of A,f . s1,f . s2 ) )
defpred S₁[ set , SortSymbol of S', SortSymbol of S'] means ( TranslationRel S reduces f . $2,f . $3 & $1 is Translation of A,f . $2,f . $3 );
A3: for s being SortSymbol of S' holds S₁[ id (the Sorts of B . s),s,s]

proof

let s be SortSymbol of S'; :: thesis: S₁[ id (the Sorts of B . s),s,s]
thus TranslationRel S reduces f . s,f . s by REWRITE1:13; :: thesis: id (the Sorts of B . s) is Translation of A,f . s,f . s
the Sorts of B = the Sorts of A * f by A1, A2, Def3;
then the Sorts of B . s = the Sorts of A . (f . s) by FUNCT_2:21;
hence id (the Sorts of B . s) is Translation of A,f . s,f . s by MSUALG_6:16; :: thesis: verum

end;

A4: for s1, s2, s3 being SortSymbol of S' st TranslationRel S' reduces s1,s2 holds
for t being Translation of B,s1,s2 st S₁[t,s1,s2] holds
for h being Function st h is_e.translation_of B,s2,s3 holds
S₁[h * t,s1,s3]

proof

let s1, s2, s3 be SortSymbol of S'; :: thesis: ( TranslationRel S' reduces s1,s2 implies for t being Translation of B,s1,s2 st S₁[t,s1,s2] holds
for h being Function st h is_e.translation_of B,s2,s3 holds
S₁[h * t,s1,s3] )
assume TranslationRel S' reduces s1,s2 ; :: thesis: for t being Translation of B,s1,s2 st S₁[t,s1,s2] holds
for h being Function st h is_e.translation_of B,s2,s3 holds
S₁[h * t,s1,s3]
let t be Translation of B,s1,s2; :: thesis: ( S₁[t,s1,s2] implies for h being Function st h is_e.translation_of B,s2,s3 holds
S₁[h * t,s1,s3] )
assume A5: S₁[t,s1,s2] ; :: thesis: for h being Function st h is_e.translation_of B,s2,s3 holds
S₁[h * t,s1,s3]
let h be Function; :: thesis: ( h is_e.translation_of B,s2,s3 implies S₁[h * t,s1,s3] )
assume A6: h is_e.translation_of B,s2,s3 ; :: thesis: S₁[h * t,s1,s3]
then A7: h is_e.translation_of A,f . s2,f . s3 by A1, A2, Th37;
[(f . s2),(f . s3)] in TranslationRel S by A1, A2, A6, Th37, MSUALG_6:12;
then TranslationRel S reduces f . s2,f . s3 by REWRITE1:16;
hence S₁[h * t,s1,s3] by A5, A7, MSUALG_6:19, REWRITE1:17; :: thesis: verum

end;

A8: for s1, s2 being SortSymbol of S' st TranslationRel S' reduces s1,s2 holds
for t being Translation of B,s1,s2 holds S₁[t,s1,s2] from MSUALG_6:sch 1(A3, A4);
let s1, s2 be SortSymbol of S'; :: thesis: ( TranslationRel S' reduces s1,s2 implies ( TranslationRel S reduces f . s1,f . s2 & ( for t being Translation of B,s1,s2 holds t is Translation of A,f . s1,f . s2 ) ) )
assume TranslationRel S' reduces s1,s2 ; :: thesis: ( TranslationRel S reduces f . s1,f . s2 & ( for t being Translation of B,s1,s2 holds t is Translation of A,f . s1,f . s2 ) )
hence ( TranslationRel S reduces f . s1,f . s2 & ( for t being Translation of B,s1,s2 holds t is Translation of A,f . s1,f . s2 ) ) by A8; :: thesis: verum