let S, S9 be non empty non void ManySortedSign ; :: thesis: for A being non-empty MSAlgebra over S
for f being Function of the carrier of S9, the carrier of S
for g being Function st f,g form_morphism_between S9,S holds
for B being non-empty MSAlgebra over S9 st B = A | (S9,f,g) holds
for s1, s2 being SortSymbol of S9 st TranslationRel S9 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 over S; :: thesis: for f being Function of the carrier of S9, the carrier of S
for g being Function st f,g form_morphism_between S9,S holds
for B being non-empty MSAlgebra over S9 st B = A | (S9,f,g) holds
for s1, s2 being SortSymbol of S9 st TranslationRel S9 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 S9, the carrier of S; :: thesis: for g being Function st f,g form_morphism_between S9,S holds
for B being non-empty MSAlgebra over S9 st B = A | (S9,f,g) holds
for s1, s2 being SortSymbol of S9 st TranslationRel S9 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 S9,S implies for B being non-empty MSAlgebra over S9 st B = A | (S9,f,g) holds
for s1, s2 being SortSymbol of S9 st TranslationRel S9 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 S9,S ; :: thesis: for B being non-empty MSAlgebra over S9 st B = A | (S9,f,g) holds
for s1, s2 being SortSymbol of S9 st TranslationRel S9 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 S9, SortSymbol of S9] means ( TranslationRel S reduces f . $2,f . $3 & $1 is Translation of A,f . $2,f . $3 );
let B be non-empty MSAlgebra over S9; :: thesis: ( B = A | (S9,f,g) implies for s1, s2 being SortSymbol of S9 st TranslationRel S9 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 | (S9,f,g) ; :: thesis: for s1, s2 being SortSymbol of S9 st TranslationRel S9 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 ) )
A3: for s1, s2, s3 being SortSymbol of S9 st TranslationRel S9 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 S9; :: thesis: ( TranslationRel S9 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 S9 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 A4: 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 A5: h is_e.translation_of B,s2,s3 ; :: thesis: S₁[h * t,s1,s3]
then [(f . s2),(f . s3)] in TranslationRel S by A1, A2, Th36, MSUALG_6:12;
then A6: TranslationRel S reduces f . s2,f . s3 by REWRITE1:15;
h is_e.translation_of A,f . s2,f . s3 by A1, A2, A5, Th36;
hence S₁[h * t,s1,s3] by A4, A6, MSUALG_6:19, REWRITE1:16; :: thesis: verum

end;

let s1, s2 be SortSymbol of S9; :: thesis: ( TranslationRel S9 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 A7: TranslationRel S9 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 ) )
A8: for s being SortSymbol of S9 holds S₁[ id ( the Sorts of B . s),s,s]

proof

let s be SortSymbol of S9; :: thesis: S₁[ id ( the Sorts of B . s),s,s]
thus TranslationRel S reduces f . s,f . s by REWRITE1:12; :: 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:15;
hence id ( the Sorts of B . s) is Translation of A,f . s,f . s by MSUALG_6:16; :: thesis: verum

end;

for s1, s2 being SortSymbol of S9 st TranslationRel S9 reduces s1,s2 holds
for t being Translation of B,s1,s2 holds S₁[t,s1,s2] from MSUALG_6:sch 1(A8, A3);
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 A7; :: thesis: verum