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_{1}[ 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_{1}[t,s1,s2] holds

for h being Function st h is_e.translation_of B,s2,s3 holds

S_{1}[h * t,s1,s3]

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_{1}[ id ( the Sorts of B . s),s,s]

for t being Translation of B,s1,s2 holds S_{1}[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

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

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

for h being Function st h is_e.translation_of B,s2,s3 holds

S

proof

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 ) ) )
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_{1}[t,s1,s2] holds

for h being Function st h is_e.translation_of B,s2,s3 holds

S_{1}[h * t,s1,s3] )

assume TranslationRel S9 reduces s1,s2 ; :: thesis: for t being Translation of B,s1,s2 st S_{1}[t,s1,s2] holds

for h being Function st h is_e.translation_of B,s2,s3 holds

S_{1}[h * t,s1,s3]

let t be Translation of B,s1,s2; :: thesis: ( S_{1}[t,s1,s2] implies for h being Function st h is_e.translation_of B,s2,s3 holds

S_{1}[h * t,s1,s3] )

assume A4: S_{1}[t,s1,s2]
; :: thesis: for h being Function st h is_e.translation_of B,s2,s3 holds

S_{1}[h * t,s1,s3]

let h be Function; :: thesis: ( h is_e.translation_of B,s2,s3 implies S_{1}[h * t,s1,s3] )

assume A5: h is_e.translation_of B,s2,s3 ; :: thesis: S_{1}[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_{1}[h * t,s1,s3]
by A4, A6, MSUALG_6:19, REWRITE1:16; :: thesis: verum

end;for h being Function st h is_e.translation_of B,s2,s3 holds

S

assume TranslationRel S9 reduces s1,s2 ; :: thesis: for t being Translation of B,s1,s2 st S

for h being Function st h is_e.translation_of B,s2,s3 holds

S

let t be Translation of B,s1,s2; :: thesis: ( S

S

assume A4: S

S

let h be Function; :: thesis: ( h is_e.translation_of B,s2,s3 implies S

assume A5: h is_e.translation_of B,s2,s3 ; :: thesis: S

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

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

proof

for s1, s2 being SortSymbol of S9 st TranslationRel S9 reduces s1,s2 holds
let s be SortSymbol of S9; :: thesis: S_{1}[ 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;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

for t being Translation of B,s1,s2 holds S

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