let S be non empty non void ManySortedSign ; :: thesis: for A being non-empty MSAlgebra over S
for s1, s2 being SortSymbol of S
for f being Function st f is_e.translation_of A,s1,s2 holds
( TranslationRel S reduces s1,s2 & f is Translation of A,s1,s2 )
let A be non-empty MSAlgebra over S; :: thesis: for s1, s2 being SortSymbol of S
for f being Function st f is_e.translation_of A,s1,s2 holds
( TranslationRel S reduces s1,s2 & f is Translation of A,s1,s2 )
let s1, s2 be SortSymbol of S; :: thesis: for f being Function st f is_e.translation_of A,s1,s2 holds
( TranslationRel S reduces s1,s2 & f is Translation of A,s1,s2 )
let f be Function; :: thesis: ( f is_e.translation_of A,s1,s2 implies ( TranslationRel S reduces s1,s2 & f is Translation of A,s1,s2 ) )
A1: len <*s1,s2*> = 1 + 1 by FINSEQ_1:44;
A2: len <*f*> = 1 by FINSEQ_1:40;
assume A3: f is_e.translation_of A,s1,s2 ; :: thesis: ( TranslationRel S reduces s1,s2 & f is Translation of A,s1,s2 )
then reconsider g = f as Function of ( the Sorts of A . s1),( the Sorts of A . s2) by Th11;
A4: <*s1,s2*> . 2 = s2 ;
A5: <*s1,s2*> . 1 = s1 ;

A6: now :: thesis: for i being Element of NAT
for g being Function
for w1, w2 being SortSymbol of S st i in dom <*f*> & g = <*f*> . i & w1 = <*s1,s2*> . i & w2 = <*s1,s2*> . (i + 1) holds
g is_e.translation_of A,w1,w2

let i be Element of NAT ; :: thesis: for g being Function
for w1, w2 being SortSymbol of S st i in dom <*f*> & g = <*f*> . i & w1 = <*s1,s2*> . i & w2 = <*s1,s2*> . (i + 1) holds
g is_e.translation_of A,w1,w2
let g be Function; :: thesis: for w1, w2 being SortSymbol of S st i in dom <*f*> & g = <*f*> . i & w1 = <*s1,s2*> . i & w2 = <*s1,s2*> . (i + 1) holds
g is_e.translation_of A,w1,w2
let w1, w2 be SortSymbol of S; :: thesis: ( i in dom <*f*> & g = <*f*> . i & w1 = <*s1,s2*> . i & w2 = <*s1,s2*> . (i + 1) implies g is_e.translation_of A,w1,w2 )
assume i in dom <*f*> ; :: thesis: ( g = <*f*> . i & w1 = <*s1,s2*> . i & w2 = <*s1,s2*> . (i + 1) implies g is_e.translation_of A,w1,w2 )
then i in {1} by FINSEQ_1:2, FINSEQ_1:38;
then i = 1 by TARSKI:def 1;
hence ( g = <*f*> . i & w1 = <*s1,s2*> . i & w2 = <*s1,s2*> . (i + 1) implies g is_e.translation_of A,w1,w2 ) by A3; :: thesis: verum

end;

dom g = the Sorts of A . s1 by FUNCT_2:def 1;
then A7: g = compose (<*f*>,( the Sorts of A . s1)) by FUNCT_7:46;
A8: [s1,s2] in TranslationRel S by A3, Th12;
hence A9: TranslationRel S reduces s1,s2 by REWRITE1:15; :: thesis: f is Translation of A,s1,s2
<*s1,s2*> is RedSequence of TranslationRel S by A8, REWRITE1:7;
hence f is Translation of A,s1,s2 by A7, A9, A1, A2, A5, A4, A6, Def6; :: thesis: verum