consider q being RedSequence of TranslationRel S such that
A2: ( q . 1 = s1 & q . (len q) = s2 ) by A1, REWRITE1:def 3;
len q >= 0 + 1 by NAT_1:13;
then consider n being Nat such that
A3: len q = 1 + n by NAT_1:10;
reconsider n = n as Element of NAT by ORDINAL1:def 13;
A4: dom q = Seg (len q) by FINSEQ_1:def 3;
defpred S₁[ set , set ] means ex f being Function ex s1, s2 being SortSymbol of S ex i being Element of NAT st
( $2 = f & i = $1 & s1 = q . i & s2 = q . (i + 1) & f is_e.translation_of A,s1,s2 );
A5: for x being set st x in Seg n holds
ex y being set st S₁[x,y]

proof

let x be set ; :: thesis: ( x in Seg n implies ex y being set st S₁[x,y] )
assume A6: x in Seg n ; :: thesis: ex y being set st S₁[x,y]
then reconsider i = x as Element of NAT ;
A7: ( i >= 1 & i <= n ) by A6, FINSEQ_1:3;
then ( i <= n + 1 & i + 1 <= len q & i + 1 >= 1 ) by A3, NAT_1:13, XREAL_1:8;
then ( i in dom q & i + 1 in dom q ) by A3, A4, A7, FINSEQ_1:3;
then A8: [(q . i),(q . (i + 1))] in TranslationRel S by REWRITE1:def 2;
then reconsider s1 = q . i, s2 = q . (i + 1) as SortSymbol of S by ZFMISC_1:106;
consider o being OperSymbol of S such that
A9: the_result_sort_of o = s2 and
A10: ex i being Element of NAT st
( i in dom (the_arity_of o) & (the_arity_of o) /. i = s1 ) by A8, Def3;
consider j being Element of NAT such that
A11: ( j in dom (the_arity_of o) & (the_arity_of o) /. j = s1 ) by A10;
consider a being Element of Args o,A;
take transl o,j,a,A ; :: thesis: S₁[x, transl o,j,a,A]
take transl o,j,a,A ; :: thesis: ex s1, s2 being SortSymbol of S ex i being Element of NAT st
( transl o,j,a,A = transl o,j,a,A & i = x & s1 = q . i & s2 = q . (i + 1) & transl o,j,a,A is_e.translation_of A,s1,s2 )
take s1 ; :: thesis: ex s2 being SortSymbol of S ex i being Element of NAT st
( transl o,j,a,A = transl o,j,a,A & i = x & s1 = q . i & s2 = q . (i + 1) & transl o,j,a,A is_e.translation_of A,s1,s2 )
take s2 ; :: thesis: ex i being Element of NAT st
( transl o,j,a,A = transl o,j,a,A & i = x & s1 = q . i & s2 = q . (i + 1) & transl o,j,a,A is_e.translation_of A,s1,s2 )
take i ; :: thesis: ( transl o,j,a,A = transl o,j,a,A & i = x & s1 = q . i & s2 = q . (i + 1) & transl o,j,a,A is_e.translation_of A,s1,s2 )
thus ( transl o,j,a,A = transl o,j,a,A & i = x & s1 = q . i & s2 = q . (i + 1) & transl o,j,a,A is_e.translation_of A,s1,s2 ) by A9, A11, Def5; :: thesis: verum

end;

consider p being Function such that
A12: ( dom p = Seg n & ( for x being set st x in Seg n holds
S₁[x,p . x] ) ) from CLASSES1:sch 1(A5);
p is Function-yielding

proof

let j be set ; :: according to FUNCOP_1:def 6 :: thesis: ( not j in dom p or p . j is set )
assume j in dom p ; :: thesis: p . j is set
then ex f being Function ex s1, s2 being SortSymbol of S ex i being Element of NAT st
( p . j = f & i = j & s1 = q . i & s2 = q . (i + 1) & f is_e.translation_of A,s1,s2 ) by A12;
hence p . j is set ; :: thesis: verum

end;

then reconsider p = p as Function-yielding FinSequence by A12, FINSEQ_1:def 2;
A13: len p = n by A12, FINSEQ_1:def 3;

A14: now

let i be Element of NAT ; :: thesis: for f being Function
for s1, s2 being SortSymbol of S st i in dom p & f = p . i & s1 = q . i & s2 = q . (i + 1) holds
f is_e.translation_of A,s1,s2
let f be Function; :: thesis: for s1, s2 being SortSymbol of S st i in dom p & f = p . i & s1 = q . i & s2 = q . (i + 1) holds
f is_e.translation_of A,s1,s2
let s1, s2 be SortSymbol of S; :: thesis: ( i in dom p & f = p . i & s1 = q . i & s2 = q . (i + 1) implies f is_e.translation_of A,s1,s2 )
assume i in dom p ; :: thesis: ( f = p . i & s1 = q . i & s2 = q . (i + 1) implies f is_e.translation_of A,s1,s2 )
then ex f being Function ex s1, s2 being SortSymbol of S ex j being Element of NAT st
( p . i = f & j = i & s1 = q . j & s2 = q . (j + 1) & f is_e.translation_of A,s1,s2 ) by A12;
hence ( f = p . i & s1 = q . i & s2 = q . (i + 1) implies f is_e.translation_of A,s1,s2 ) ; :: thesis: verum

end;

then reconsider t = compose p,(the Sorts of A . s1) as Function of (the Sorts of A . s1),(the Sorts of A . s2) by A1, A2, A3, A13, Th14;
take t ; :: thesis: ex q being RedSequence of TranslationRel S ex p being Function-yielding FinSequence st
( t = compose p,(the Sorts of A . s1) & len q = (len p) + 1 & s1 = q . 1 & s2 = q . (len q) & ( for i being Element of NAT
for f being Function
for s1, s2 being SortSymbol of S st i in dom p & f = p . i & s1 = q . i & s2 = q . (i + 1) holds
f is_e.translation_of A,s1,s2 ) )
take q ; :: thesis: ex p being Function-yielding FinSequence st
( t = compose p,(the Sorts of A . s1) & len q = (len p) + 1 & s1 = q . 1 & s2 = q . (len q) & ( for i being Element of NAT
for f being Function
for s1, s2 being SortSymbol of S st i in dom p & f = p . i & s1 = q . i & s2 = q . (i + 1) holds
f is_e.translation_of A,s1,s2 ) )
take p ; :: thesis: ( t = compose p,(the Sorts of A . s1) & len q = (len p) + 1 & s1 = q . 1 & s2 = q . (len q) & ( for i being Element of NAT
for f being Function
for s1, s2 being SortSymbol of S st i in dom p & f = p . i & s1 = q . i & s2 = q . (i + 1) holds
f is_e.translation_of A,s1,s2 ) )
thus ( t = compose p,(the Sorts of A . s1) & len q = (len p) + 1 & s1 = q . 1 & s2 = q . (len q) & ( for i being Element of NAT
for f being Function
for s1, s2 being SortSymbol of S st i in dom p & f = p . i & s1 = q . i & s2 = q . (i + 1) holds
f is_e.translation_of A,s1,s2 ) ) by A2, A3, A12, A14, FINSEQ_1:def 3; :: thesis: verum