let S be non empty non void ManySortedSign ; :: thesis: 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; :: thesis: 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; :: thesis: ( 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 ; :: thesis: 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 S₁[ 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 S₁[t,s1,s2] holds
for f being Function st f is_e.translation_of A1,s2,s3 holds
S₁[f * t,s1,s3]

proof

let s1, s2, s3 be SortSymbol of S; :: thesis: ( TranslationRel S reduces s1,s2 implies for t being Translation of A1,s1,s2 st S₁[t,s1,s2] holds
for f being Function st f is_e.translation_of A1,s2,s3 holds
S₁[f * t,s1,s3] )
assume A3: TranslationRel S reduces s1,s2 ; :: thesis: for t being Translation of A1,s1,s2 st S₁[t,s1,s2] holds
for f being Function st f is_e.translation_of A1,s2,s3 holds
S₁[f * t,s1,s3]
let t be Translation of A1,s1,s2; :: thesis: ( S₁[t,s1,s2] implies for f being Function st f is_e.translation_of A1,s2,s3 holds
S₁[f * t,s1,s3] )
given T being Translation of A2,s1,s2 such that A4: T * (h . s1) = (h . s2) * t ; :: thesis: for f being Function st f is_e.translation_of A1,s2,s3 holds
S₁[f * t,s1,s3]
let f be Function; :: thesis: ( f is_e.translation_of A1,s2,s3 implies S₁[f * t,s1,s3] )
assume f is_e.translation_of A1,s2,s3 ; :: thesis: S₁[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 ; :: thesis: 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 ; :: thesis: verum

end;

A7: for s being SortSymbol of S holds S₁[ id ( the Sorts of A1 . s),s,s]

proof

let s be SortSymbol of S; :: thesis: S₁[ id ( the Sorts of A1 . s),s,s]
A8: (id ( the Sorts of A2 . s)) * (h . s) = h . s by FUNCT_2:17;
A9: (h . s) * (id ( the Sorts of A1 . s)) = h . s by FUNCT_2:17;
id ( the Sorts of A2 . s) is Translation of A2,s,s by Th16;
hence S₁[ id ( the Sorts of A1 . s),s,s] by A8, A9; :: thesis: verum

end;

thus for s1, s2 being SortSymbol of S st TranslationRel S reduces s1,s2 holds
for t being Translation of A1,s1,s2 holds S₁[t,s1,s2] from MSUALG_6:sch 1(A7, A2); :: thesis: verum