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;
for x being set ex y being set st S1[n,x,y]let x be
set ;
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
;
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
;
S1[n,x,y]
thus
(
n < F2()
- 1 implies
P1[
n + 1,
x,
y] )
by A4;
( not n < F2() - 1 implies y = 0 )
thus
( not
n < F2()
- 1 implies
y = 0 )
by A3;
verum
end;
hence
ex
y being
set st
S1[
n,
x,
y]
;
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 ;
( x in REAL implies ex y being object st S2[x,y] )
assume
x in REAL
;
ex y being object st S2[x,y]
then reconsider r =
x as
Real ;
take
f . (r - 1)
;
S2[x,f . (r - 1)]
thus
S2[
x,
f . (r - 1)]
;
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
; ( 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; ( ( 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 )
hence
( p . 1 = F1() or F2() = 0 )
; for n being Nat st 1 <= n & n < F2() holds
P1[n,p . n,p . (n + 1)]
let n be Nat; ( 1 <= n & n < F2() implies P1[n,p . n,p . (n + 1)] )
assume that
A10:
1 <= n
and
A11:
n < F2()
; 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
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; verum