defpred S1[ Nat, set , set ] means ( ( $1 < F2() - 1 implies P1[$1 + 1,$2,$3] ) & ( not $1 < F2() - 1 implies $3 = 0 ) );
A2: for n being Nat
for x being set ex y being set st S1[n,x,y]
proof
let n be Nat; :: thesis: for x being set ex y being set st S1[n,x,y]
let x be set ; :: thesis: ex y being set st S1[n,x,y]
( n < F2() - 1 implies ex y being set st S1[n,x,y] )
proof
assume A3: n < F2() - 1 ; :: thesis: ex y being set st S1[n,x,y]
then n + 1 < F2() by XREAL_1:20;
then consider y being set such that
A4: P1[n + 1,x,y] by A1, NAT_1:11;
take y ; :: thesis: S1[n,x,y]
thus ( n < F2() - 1 implies P1[n + 1,x,y] ) by A4; :: thesis: ( not n < F2() - 1 implies y = 0 )
thus ( not n < F2() - 1 implies y = 0 ) by A3; :: thesis: verum
end;
hence ex y being set st S1[n,x,y] ; :: thesis: verum
end;
consider f being Function such that
A5: ( dom f = NAT & f . 0 = F1() & ( for n being Nat holds S1[n,f . n,f . (n + 1)] ) ) from RECDEF_1:sch 1(A2);
 defpred S2[ object , object ] means for r being Real st r = $1 holds
$2 = f . (r - 1);
A6: 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
A7: ( dom g = REAL & ( for x being object st x in REAL holds
S2[x,g . x] ) ) from CLASSES1:sch 1(A6);
 Seg F2() c= REAL by NUMBERS:19;
then A8: dom (g | (Seg F2())) = Seg F2() by A7, RELAT_1:62;
then reconsider p = g | (Seg F2()) as FinSequence by FINSEQ_1:def 2;
take p ; :: thesis: ( len p = F2() & ( p . 1 = F1() or F2() = 0 ) & ( for n being Nat st 1 <= n & n < F2() holds
P1[n,p . n,p . (n + 1)] ) )
F2() in NAT by ORDINAL1:def 12;
hence len p = F2() by A8, FINSEQ_1:def 3; :: thesis: ( ( p . 1 = F1() or F2() = 0 ) & ( for n being Nat st 1 <= n & n < F2() holds
P1[n,p . n,p . (n + 1)] ) )
( not F2() <> 0 or p . 1 = F1() or F2() = 0 )
proof
assume F2() <> 0 ; :: thesis: ( p . 1 = F1() or F2() = 0 )
then consider k being Nat such that
A9: F2() = k + 1 by NAT_1:6;
0 + 1 <= k + 1 by XREAL_1:7;
then 1 in Seg F2() by A9, FINSEQ_1:1;
then p . 1 = g . 1 by FUNCT_1:49
.= f . (1 - 1) by A7, Lm2
.= F1() by A5 ;
hence ( p . 1 = F1() or F2() = 0 ) ; :: thesis: verum
end;
hence ( p . 1 = F1() or F2() = 0 ) ; :: thesis: for n being Nat st 1 <= n & n < F2() holds
P1[n,p . n,p . (n + 1)]
let n be Nat; :: thesis: ( 1 <= n & n < F2() implies P1[n,p . n,p . (n + 1)] )
assume that
A10: 1 <= n and
A11: n < F2() ; :: thesis: P1[n,p . n,p . (n + 1)]
0 <> n by A10;
then consider k being Nat such that
A12: n = k + 1 by NAT_1:6;
A13: for n being Nat st n < F2() holds
p . (n + 1) = f . n
proof
let n be Nat; :: thesis: ( n < F2() implies p . (n + 1) = f . n )
assume n < F2() ; :: thesis: p . (n + 1) = f . n
then ( 1 <= n + 1 & n + 1 <= F2() ) by NAT_1:11, NAT_1:13;
then A14: n + 1 in Seg F2() by FINSEQ_1:1;
n + 1 in REAL by XREAL_0:def 1;
then g . (n + 1) = f . ((n + 1) - 1) by A7
.= f . n ;
hence p . (n + 1) = f . n by A14, FUNCT_1:49; :: thesis: verum
end;
reconsider k = k as Nat ;
k <= k + 1 by NAT_1:11;
then A15: k < F2() by A11, A12, XXREAL_0:2;
k < F2() - 1 by A11, A12, XREAL_1:20;
then P1[k + 1,f . k,f . (k + 1)] by A5;
then P1[k + 1,f . k,p . ((k + 1) + 1)] by A13, A11, A12;
hence P1[n,p . n,p . (n + 1)] by A13, A12, A15; :: thesis: verum