let S, S9 be non empty non void ManySortedSign ; 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; 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; 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; ( 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
; 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 S1[ 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; ( 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)
; 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 S1[t,s1,s2] holds
for h being Function st h is_e.translation_of B,s2,s3 holds
S1[h * t,s1,s3]
proof
let s1,
s2,
s3 be
SortSymbol of
S9;
( TranslationRel S9 reduces s1,s2 implies for t being Translation of B,s1,s2 st S1[t,s1,s2] holds
for h being Function st h is_e.translation_of B,s2,s3 holds
S1[h * t,s1,s3] )
assume
TranslationRel S9 reduces s1,
s2
;
for t being Translation of B,s1,s2 st S1[t,s1,s2] holds
for h being Function st h is_e.translation_of B,s2,s3 holds
S1[h * t,s1,s3]
let t be
Translation of
B,
s1,
s2;
( S1[t,s1,s2] implies for h being Function st h is_e.translation_of B,s2,s3 holds
S1[h * t,s1,s3] )
assume A4:
S1[
t,
s1,
s2]
;
for h being Function st h is_e.translation_of B,s2,s3 holds
S1[h * t,s1,s3]
let h be
Function;
( h is_e.translation_of B,s2,s3 implies S1[h * t,s1,s3] )
assume A5:
h is_e.translation_of B,
s2,
s3
;
S1[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
S1[
h * t,
s1,
s3]
by A4, A6, MSUALG_6:19, REWRITE1:16;
verum
end;
let s1, s2 be SortSymbol of S9; ( 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
; ( 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 S1[ id ( the Sorts of B . s),s,s]
for s1, s2 being SortSymbol of S9 st TranslationRel S9 reduces s1,s2 holds
for t being Translation of B,s1,s2 holds S1[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; verum