consider 00 being Element of F₁();
defpred S₁[ Element of NAT , set , set ] means ( ( 0 <= $1 & $1 <= F₃() - 2 implies P₁[$1 + 1,$2,$3] ) & ( ( not 0 <= $1 or not $1 <= F₃() - 2 ) implies $3 = 00 ) );
A2: for n being Element of NAT
for x being Element of F₁() ex y being Element of F₁() st S₁[n,x,y]

proof

let n be Element of NAT ; :: thesis: for x being Element of F₁() ex y being Element of F₁() st S₁[n,x,y]
let x be Element of F₁(); :: thesis: ex y being Element of F₁() st S₁[n,x,y]
( 0 <= n & n <= F₃() - 2 implies ex y being Element of F₁() st S₁[n,x,y] )

proof

assume A3: ( 0 <= n & n <= F₃() - 2 ) ; :: thesis: ex y being Element of F₁() st S₁[n,x,y]
then ( 0 + 1 <= n + 1 & n + 1 <= (F₃() - 2) + 1 ) by XREAL_1:8;
then consider y being Element of F₁() such that
A4: P₁[n + 1,x,y] by A1;
take y ; :: thesis: S₁[n,x,y]
thus ( 0 <= n & n <= F₃() - 2 implies P₁[n + 1,x,y] ) by A4; :: thesis: ( ( not 0 <= n or not n <= F₃() - 2 ) implies y = 00 )
thus ( ( not 0 <= n or not n <= F₃() - 2 ) implies y = 00 ) by A3; :: thesis: verum

end;

hence ex y being Element of F₁() st S₁[n,x,y] ; :: thesis: verum

end;

consider f being Function of NAT ,F₁() such that
A5: ( f . 0 = F₂() & ( for n being Element of NAT holds S₁[n,f . n,f . (n + 1)] ) ) from RECDEF_1:sch 2(A2);
defpred S₂[ set , set ] means for r being Real st r = $1 holds
$2 = f . (r - 1);
A6: for x being set st x in REAL holds
ex y being set st S₂[x,y]

proof

let x be set ; :: thesis: ( x in REAL implies ex y being set st S₂[x,y] )
assume x in REAL ; :: thesis: ex y being set st S₂[x,y]
then reconsider r = x as Real ;
take f . (r - 1) ; :: thesis: S₂[x,f . (r - 1)]
thus S₂[x,f . (r - 1)] ; :: thesis: verum

end;

consider g being Function such that
A9: ( dom g = REAL & ( for x being set st x in REAL holds
S₂[x,g . x] ) ) from CLASSES1:sch 1(A6);
Seg F₃() c= REAL by XBOOLE_1:1;
then A10: dom (g | (Seg F₃())) = Seg F₃() by A9, RELAT_1:91;
then reconsider p = g | (Seg F₃()) as FinSequence by FINSEQ_1:def 2;

now

let x be set ; :: thesis: ( x in rng p implies x in F₁() )
assume x in rng p ; :: thesis: x in F₁()
then consider y being set such that
A11: ( y in dom p & x = p . y ) by FUNCT_1:def 5;
reconsider y = y as Element of NAT by A11;
A12: f . (y - 1) in F₁()

proof

y <> 0 by A10, A11, FINSEQ_1:3;
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 13;
f . k in F₁() ;
hence f . (y - 1) in F₁() by A13; :: thesis: verum

end;

p . y = g . y by A11, FUNCT_1:70;
hence x in F₁() by A9, A11, A12; :: thesis: verum

end;

then rng p c= F₁() by TARSKI:def 3;
then reconsider p = p as FinSequence of F₁() by FINSEQ_1:def 4;
take p ; :: thesis: ( len p = F₃() & ( p /. 1 = F₂() or F₃() = 0 ) & ( for n being Element of NAT st 1 <= n & n <= F₃() - 1 holds
P₁[n,p /. n,p /. (n + 1)] ) )
thus len p = F₃() by A10, FINSEQ_1:def 3; :: thesis: ( ( p /. 1 = F₂() or F₃() = 0 ) & ( for n being Element of NAT st 1 <= n & n <= F₃() - 1 holds
P₁[n,p /. n,p /. (n + 1)] ) )
A14: for n being Element of NAT st n <= F₃() - 1 holds
p /. (n + 1) = f . n

proof

let n be Element of NAT ; :: thesis: ( n <= F₃() - 1 implies p /. (n + 1) = f . n )
assume A15: n <= F₃() - 1 ; :: thesis: p /. (n + 1) = f . n
A16: 1 <= n + 1 by NAT_1:11;
n + 1 <= (F₃() - 1) + 1 by A15, XREAL_1:8;
then A17: n + 1 in Seg F₃() by A16, FINSEQ_1:3;
A18: g . (n + 1) = f . ((n + 1) - 1) by A9
.= f . n ;
p /. (n + 1) = p . (n + 1) by A10, A17, PARTFUN1:def 8;
hence p /. (n + 1) = f . n by A17, A18, FUNCT_1:72; :: thesis: verum

end;

thus ( p /. 1 = F₂() or F₃() = 0 ) :: thesis: for n being Element of NAT st 1 <= n & n <= F₃() - 1 holds
P₁[n,p /. n,p /. (n + 1)]

proof

( not F₃() <> 0 or p /. 1 = F₂() or F₃() = 0 )

proof

assume F₃() <> 0 ; :: thesis: ( p /. 1 = F₂() or F₃() = 0 )
then consider k being Nat such that
A19: F₃() = k + 1 by NAT_1:6;
0 + 1 <= k + 1 by XREAL_1:9;
then A20: 1 in Seg F₃() by A19, FINSEQ_1:3;
then p /. 1 = p . 1 by A10, PARTFUN1:def 8
.= g . 1 by A20, FUNCT_1:72
.= f . (1 - 1) by A9
.= F₂() by A5 ;
hence ( p /. 1 = F₂() or F₃() = 0 ) ; :: thesis: verum

end;

hence ( p /. 1 = F₂() or F₃() = 0 ) ; :: thesis: verum

end;

let n be Element of NAT ; :: thesis: ( 1 <= n & n <= F₃() - 1 implies P₁[n,p /. n,p /. (n + 1)] )
assume A21: ( 1 <= n & n <= F₃() - 1 ) ; :: thesis: P₁[n,p /. n,p /. (n + 1)]
then consider k being Nat such that
A22: n = k + 1 by NAT_1:6;
A23: k in NAT by ORDINAL1:def 13;
( 0 <= k & k <= (F₃() - 1) - 1 ) by A21, A22, XREAL_1:21;
then P₁[k + 1,f . k,f . (k + 1)] by A5, A23;
then A24: P₁[k + 1,f . k,p /. ((k + 1) + 1)] by A14, A21, A22;
k <= k + 1 by NAT_1:11;
hence P₁[n,p /. n,p /. (n + 1)] by A14, A21, A22, A23, A24, XXREAL_0:2; :: thesis: verum