consider q being RedSequence of TranslationRel S such that
A2: q . 1 = s1 and
A3: q . (len q) = s2 by A1;
defpred S₁[ object , object ] 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
A4: len q = 1 + n by NAT_1:10;
reconsider n = n as Element of NAT by ORDINAL1:def 12;
A5: dom q = Seg (len q) by FINSEQ_1:def 3;
A6: for x being object st x in Seg n holds
ex y being object st S₁[x,y]

proof

let x be object ; :: thesis: ( x in Seg n implies ex y being object st S₁[x,y] )
assume A7: x in Seg n ; :: thesis: ex y being object st S₁[x,y]
then reconsider i = x as Element of NAT ;
A8: i <= n by A7, FINSEQ_1:1;
then A9: i + 1 <= len q by A4, XREAL_1:6;
A10: i >= 1 by A7, FINSEQ_1:1;
then i + 1 >= 1 by NAT_1:13;
then A11: i + 1 in dom q by A5, A9, FINSEQ_1:1;
i <= n + 1 by A8, NAT_1:13;
then i in dom q by A4, A5, A10, FINSEQ_1:1;
then A12: [(q . i),(q . (i + 1))] in TranslationRel S by A11, 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
A13: the_result_sort_of o = s2 and
A14: ex i being Element of NAT st
( i in dom (the_arity_of o) & (the_arity_of o) /. i = s1 ) by A12, Def3;
set a = the Element of Args (o,A);
consider j being Element of NAT such that
A15: j in dom (the_arity_of o) and
A16: (the_arity_of o) /. j = s1 by A14;
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 A13, A15, A16; :: thesis: verum

end;

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

proof

let j be object ; :: 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 A17;
hence p . j is set ; :: thesis: verum

end;

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

A18: 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 A17;
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 A17, 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 A2, A3, A4, A18, 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, A4, A17, A18, FINSEQ_1:def 3; :: thesis: verum