let S be non empty non void ManySortedSign ; for A1, A2 being non-empty MSAlgebra over S
for h being ManySortedFunction of A1,A2 st h is_homomorphism A1,A2 holds
for s1, s2 being SortSymbol of S st TranslationRel S reduces s1,s2 holds
for t being Translation of A1,s1,s2 ex T being Translation of A2,s1,s2 st T * (h . s1) = (h . s2) * t
let A1, A2 be non-empty MSAlgebra over S; for h being ManySortedFunction of A1,A2 st h is_homomorphism A1,A2 holds
for s1, s2 being SortSymbol of S st TranslationRel S reduces s1,s2 holds
for t being Translation of A1,s1,s2 ex T being Translation of A2,s1,s2 st T * (h . s1) = (h . s2) * t
let h be ManySortedFunction of A1,A2; ( h is_homomorphism A1,A2 implies for s1, s2 being SortSymbol of S st TranslationRel S reduces s1,s2 holds
for t being Translation of A1,s1,s2 ex T being Translation of A2,s1,s2 st T * (h . s1) = (h . s2) * t )
assume A1:
h is_homomorphism A1,A2
; for s1, s2 being SortSymbol of S st TranslationRel S reduces s1,s2 holds
for t being Translation of A1,s1,s2 ex T being Translation of A2,s1,s2 st T * (h . s1) = (h . s2) * t
defpred S1[ Function, SortSymbol of S, SortSymbol of S] means ex T being Translation of A2,$2,$3 st T * (h . $2) = (h . $3) * $1;
A2:
for s1, s2, s3 being SortSymbol of S st TranslationRel S reduces s1,s2 holds
for t being Translation of A1,s1,s2 st S1[t,s1,s2] holds
for f being Function st f is_e.translation_of A1,s2,s3 holds
S1[f * t,s1,s3]
proof
let s1,
s2,
s3 be
SortSymbol of
S;
( TranslationRel S reduces s1,s2 implies for t being Translation of A1,s1,s2 st S1[t,s1,s2] holds
for f being Function st f is_e.translation_of A1,s2,s3 holds
S1[f * t,s1,s3] )
assume A3:
TranslationRel S reduces s1,
s2
;
for t being Translation of A1,s1,s2 st S1[t,s1,s2] holds
for f being Function st f is_e.translation_of A1,s2,s3 holds
S1[f * t,s1,s3]
let t be
Translation of
A1,
s1,
s2;
( S1[t,s1,s2] implies for f being Function st f is_e.translation_of A1,s2,s3 holds
S1[f * t,s1,s3] )
given T being
Translation of
A2,
s1,
s2 such that A4:
T * (h . s1) = (h . s2) * t
;
for f being Function st f is_e.translation_of A1,s2,s3 holds
S1[f * t,s1,s3]
let f be
Function;
( f is_e.translation_of A1,s2,s3 implies S1[f * t,s1,s3] )
assume
f is_e.translation_of A1,
s2,
s3
;
S1[f * t,s1,s3]
then consider T1 being
Function of
( the Sorts of A2 . s2),
( the Sorts of A2 . s3) such that A5:
T1 is_e.translation_of A2,
s2,
s3
and A6:
T1 * (h . s2) = (h . s3) * f
by A1, Th23;
reconsider T2 =
T1 * T as
Translation of
A2,
s1,
s3 by A3, A5, Th19;
take
T2
;
T2 * (h . s1) = (h . s3) * (f * t)
thus T2 * (h . s1) =
T1 * (T * (h . s1))
by RELAT_1:36
.=
((h . s3) * f) * t
by A4, A6, RELAT_1:36
.=
(h . s3) * (f * t)
by RELAT_1:36
;
verum
end;
A7:
for s being SortSymbol of S holds S1[ id ( the Sorts of A1 . s),s,s]
thus
for s1, s2 being SortSymbol of S st TranslationRel S reduces s1,s2 holds
for t being Translation of A1,s1,s2 holds S1[t,s1,s2]
from MSUALG_6:sch 1(A7, A2); verum