set 00 = the Element of F1();
defpred S1[ Nat, set , set ] means ( ( 0 <= \$1 & \$1 <= F3() - 2 implies P1[\$1 + 1,\$2,\$3] ) & ( ( not 0 <= \$1 or not \$1 <= F3() - 2 ) implies \$3 = the Element of F1() ) );
A2: for n being Nat
for x being Element of F1() ex y being Element of F1() st S1[n,x,y]
proof
let n be Nat; :: thesis: for x being Element of F1() ex y being Element of F1() st S1[n,x,y]
let x be Element of F1(); :: thesis: ex y being Element of F1() st S1[n,x,y]
( 0 <= n & n <= F3() - 2 implies ex y being Element of F1() st S1[n,x,y] )
proof
A3: 0 + 1 <= n + 1 by XREAL_1:6;
assume that
0 <= n and
A4: n <= F3() - 2 ; :: thesis: ex y being Element of F1() st S1[n,x,y]
n + 1 <= (F3() - 2) + 1 by ;
then consider y being Element of F1() such that
A5: P1[n + 1,x,y] by A1, A3;
take y ; :: thesis: S1[n,x,y]
thus ( 0 <= n & n <= F3() - 2 implies P1[n + 1,x,y] ) by A5; :: thesis: ( ( not 0 <= n or not n <= F3() - 2 ) implies y = the Element of F1() )
thus ( ( not 0 <= n or not n <= F3() - 2 ) implies y = the Element of F1() ) by A4; :: thesis: verum
end;
hence ex y being Element of F1() st S1[n,x,y] ; :: thesis: verum
end;
consider f being sequence of F1() such that
A6: ( f . 0 = F2() & ( for n being Nat holds S1[n,f . n,f . (n + 1)] ) ) from defpred S2[ object , object ] means for r being Real st r = \$1 holds
\$2 = f . (r - 1);
A7: for x being object st x in REAL holds
ex y being object st S2[x,y]
proof
let x be object ; :: thesis: ( x in REAL implies ex y being object st S2[x,y] )
assume x in REAL ; :: thesis: ex y being object st S2[x,y]
then reconsider r = x as Real ;
take f . (r - 1) ; :: thesis: S2[x,f . (r - 1)]
thus S2[x,f . (r - 1)] ; :: thesis: verum
end;
consider g being Function such that
A8: ( dom g = REAL & ( for x being object st x in REAL holds
S2[x,g . x] ) ) from Seg F3() c= REAL by NUMBERS:19;
then A9: dom (g | (Seg F3())) = Seg F3() by ;
then reconsider p = g | (Seg F3()) as FinSequence by FINSEQ_1:def 2;
now :: thesis: for x being object st x in rng p holds
x in F1()
let x be object ; :: thesis: ( x in rng p implies x in F1() )
assume x in rng p ; :: thesis: x in F1()
then consider y being object such that
A10: y in dom p and
A11: x = p . y by FUNCT_1:def 3;
reconsider y = y as Element of NAT by A10;
A12: f . (y - 1) in F1()
proof
y <> 0 by ;
then consider k being Nat such that
A13: y = k + 1 by NAT_1:6;
reconsider k = k as Element of NAT by ORDINAL1:def 12;
f . k in F1() ;
hence f . (y - 1) in F1() by A13; :: thesis: verum
end;
A14: y in REAL by XREAL_0:def 1;
p . y = g . y by ;
hence x in F1() by A8, A11, A12, A14; :: thesis: verum
end;
then rng p c= F1() ;
then reconsider p = p as FinSequence of F1() by FINSEQ_1:def 4;
take p ; :: thesis: ( len p = F3() & ( p /. 1 = F2() or F3() = 0 ) & ( for n being Nat st 1 <= n & n <= F3() - 1 holds
P1[n,p /. n,p /. (n + 1)] ) )

thus len p = F3() by ; :: thesis: ( ( p /. 1 = F2() or F3() = 0 ) & ( for n being Nat st 1 <= n & n <= F3() - 1 holds
P1[n,p /. n,p /. (n + 1)] ) )

( F3() <> 0 implies p /. 1 = F2() )
proof
assume F3() <> 0 ; :: thesis: p /. 1 = F2()
then consider k being Nat such that
A15: F3() = k + 1 by NAT_1:6;
0 + 1 <= k + 1 by XREAL_1:7;
then A16: 1 in Seg F3() by ;
then p /. 1 = p . 1 by
.= g . 1 by
.= f . (1 - 1) by
.= F2() by A6 ;
hence p /. 1 = F2() ; :: thesis: verum
end;
hence ( p /. 1 = F2() or F3() = 0 ) ; :: thesis: for n being Nat st 1 <= n & n <= F3() - 1 holds
P1[n,p /. n,p /. (n + 1)]

let n be Nat; :: thesis: ( 1 <= n & n <= F3() - 1 implies P1[n,p /. n,p /. (n + 1)] )
assume that
A17: 1 <= n and
A18: n <= F3() - 1 ; :: thesis: P1[n,p /. n,p /. (n + 1)]
consider k being Nat such that
A19: n = k + 1 by ;
A20: for n being Nat st n <= F3() - 1 holds
p /. (n + 1) = f . n
proof
let n be Nat; :: thesis: ( n <= F3() - 1 implies p /. (n + 1) = f . n )
assume n <= F3() - 1 ; :: thesis: p /. (n + 1) = f . n
then A21: n + 1 <= (F3() - 1) + 1 by XREAL_1:6;
n + 1 in REAL by XREAL_0:def 1;
then A22: g . (n + 1) = f . ((n + 1) - 1) by A8
.= f . n ;
1 <= n + 1 by NAT_1:11;
then A23: n + 1 in Seg F3() by ;
then p /. (n + 1) = p . (n + 1) by ;
hence p /. (n + 1) = f . n by ; :: thesis: verum
end;
A24: k <= k + 1 by NAT_1:11;
k <= (F3() - 1) - 1 by ;
then P1[k + 1,f . k,f . (k + 1)] by A6;
then P1[k + 1,f . k,p /. ((k + 1) + 1)] by ;
hence P1[n,p /. n,p /. (n + 1)] by ; :: thesis: verum