consider q being RedSequence of TranslationRel S such that
A1: q . 1 = s1 and
A2: q . (len q) = s2 by B1, REWRITE1: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 );
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 12;
A4: dom q = Seg (len q) by FINSEQ_1:def 3;
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 <= n by A6, FINSEQ_1:1;
then A8: i + 1 <= len q by A3, XREAL_1:6;
A9: i >= 1 by A6, FINSEQ_1:1;
then i + 1 >= 1 by NAT_1:13;
then A10: i + 1 in dom q by A4, A8, FINSEQ_1:1;
i <= n + 1 by A7, NAT_1:13;
then i in dom q by A3, A4, A9, FINSEQ_1:1;
then A11: [(q . i),(q . (i + 1))] in TranslationRel S by A10, REWRITE1:def 2;
then reconsider s1 = q . i, s2 = q . (i + 1) as SortSymbol of S by ZFMISC_1:87;
consider o being OperSymbol of S such that
A12: the_result_sort_of o = s2 and
A13: ex i being Element of NAT st
( i in dom (the_arity_of o) & (the_arity_of o) /. i = s1 ) by A11, Def3;
set a = the Element of Args (o,A);
consider j being Element of NAT such that
A14: j in dom (the_arity_of o) and
A15: (the_arity_of o) /. j = s1 by A13;
take transl (o,j, the Element of Args (o,A),A) ; :: thesis: S₁[x, transl (o,j, the Element of Args (o,A),A)]
take transl (o,j, the Element of Args (o,A),A) ; :: thesis: ex s1, s2 being SortSymbol of S ex i being Element of NAT st
( transl (o,j, the Element of Args (o,A),A) = transl (o,j, the Element of Args (o,A),A) & i = x & s1 = q . i & s2 = q . (i + 1) & transl (o,j, the Element of Args (o,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, the Element of Args (o,A),A) = transl (o,j, the Element of Args (o,A),A) & i = x & s1 = q . i & s2 = q . (i + 1) & transl (o,j, the Element of Args (o,A),A) is_e.translation_of A,s1,s2 )
take s2 ; :: thesis: ex i being Element of NAT st
( transl (o,j, the Element of Args (o,A),A) = transl (o,j, the Element of Args (o,A),A) & i = x & s1 = q . i & s2 = q . (i + 1) & transl (o,j, the Element of Args (o,A),A) is_e.translation_of A,s1,s2 )
take i ; :: thesis: ( transl (o,j, the Element of Args (o,A),A) = transl (o,j, the Element of Args (o,A),A) & i = x & s1 = q . i & s2 = q . (i + 1) & transl (o,j, the Element of Args (o,A),A) is_e.translation_of A,s1,s2 )
thus ( transl (o,j, the Element of Args (o,A),A) = transl (o,j, the Element of Args (o,A),A) & i = x & s1 = q . i & s2 = q . (i + 1) & transl (o,j, the Element of Args (o,A),A) is_e.translation_of A,s1,s2 ) by A12, A14, A15, Def5; :: thesis: verum

end;

consider p being Function such that
A16: ( 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 proj1 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 A16;
hence p . j is set ; :: thesis: verum

end;

then reconsider p = p as Function-yielding FinSequence by A16, FINSEQ_1:def 2;

A17: now :: thesis: 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

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 A16;
hence ( f = p . i & s1 = q . i & s2 = q . (i + 1) implies f is_e.translation_of A,s1,s2 ) ; :: thesis: verum

end;

len p = n by A16, FINSEQ_1:def 3;
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, A17, 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 A1, A2, A3, A16, A17, FINSEQ_1:def 3; :: thesis: verum