let S be non empty non void ManySortedSign ; 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; 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; 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; ( 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
; ( 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
by FINSEQ_1:44;
A5:
<*s1,s2*> . 1 = s1
by FINSEQ_1:44;
A6:
now 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,w2let i be
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,w2let g be
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,w2let w1,
w2 be
SortSymbol of
S;
( 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*>
;
( 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, A5, A4, FINSEQ_1:40;
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; 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; verum