defpred S_{1}[ Nat, set , set ] means ( ( $1 < F_{2}() - 1 implies P_{1}[$1 + 1,$2,$3] ) & ( not $1 < F_{2}() - 1 implies $3 = 0 ) );

A2: for n being Nat

for x being set ex y being set st S_{1}[n,x,y]

A5: ( dom f = NAT & f . 0 = F_{1}() & ( for n being Nat holds S_{1}[n,f . n,f . (n + 1)] ) )
from RECDEF_1:sch 1(A2);

defpred S_{2}[ 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 S_{2}[x,y]

A7: ( dom g = REAL & ( for x being object st x in REAL holds

S_{2}[x,g . x] ) )
from CLASSES1:sch 1(A6);

Seg F_{2}() c= REAL
by NUMBERS:19;

then A8: dom (g | (Seg F_{2}())) = Seg F_{2}()
by A7, RELAT_1:62;

then reconsider p = g | (Seg F_{2}()) as FinSequence by FINSEQ_1:def 2;

take p ; :: thesis: ( len p = F_{2}() & ( p . 1 = F_{1}() or F_{2}() = 0 ) & ( for n being Nat st 1 <= n & n < F_{2}() holds

P_{1}[n,p . n,p . (n + 1)] ) )

F_{2}() in NAT
by ORDINAL1:def 12;

hence len p = F_{2}()
by A8, FINSEQ_1:def 3; :: thesis: ( ( p . 1 = F_{1}() or F_{2}() = 0 ) & ( for n being Nat st 1 <= n & n < F_{2}() holds

P_{1}[n,p . n,p . (n + 1)] ) )

( not F_{2}() <> 0 or p . 1 = F_{1}() or F_{2}() = 0 )
_{1}() or F_{2}() = 0 )
; :: thesis: for n being Nat st 1 <= n & n < F_{2}() holds

P_{1}[n,p . n,p . (n + 1)]

let n be Nat; :: thesis: ( 1 <= n & n < F_{2}() implies P_{1}[n,p . n,p . (n + 1)] )

assume that

A10: 1 <= n and

A11: n < F_{2}()
; :: thesis: P_{1}[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 < F_{2}() holds

p . (n + 1) = f . n

k <= k + 1 by NAT_1:11;

then A15: k < F_{2}()
by A11, A12, XXREAL_0:2;

k < F_{2}() - 1
by A11, A12, XREAL_1:20;

then P_{1}[k + 1,f . k,f . (k + 1)]
by A5;

then P_{1}[k + 1,f . k,p . ((k + 1) + 1)]
by A13, A11, A12;

hence P_{1}[n,p . n,p . (n + 1)]
by A13, A12, A15; :: thesis: verum

A2: for n being Nat

for x being set ex y being set st S

proof

consider f being Function such that
let n be Nat; :: thesis: for x being set ex y being set st S_{1}[n,x,y]

let x be set ; :: thesis: ex y being set st S_{1}[n,x,y]

( n < F_{2}() - 1 implies ex y being set st S_{1}[n,x,y] )
_{1}[n,x,y]
; :: thesis: verum

end;let x be set ; :: thesis: ex y being set st S

( n < F

proof

hence
ex y being set st S
assume A3:
n < F_{2}() - 1
; :: thesis: ex y being set st S_{1}[n,x,y]

then n + 1 < F_{2}()
by XREAL_1:20;

then consider y being set such that

A4: P_{1}[n + 1,x,y]
by A1, NAT_1:11;

take y ; :: thesis: S_{1}[n,x,y]

thus ( n < F_{2}() - 1 implies P_{1}[n + 1,x,y] )
by A4; :: thesis: ( not n < F_{2}() - 1 implies y = 0 )

thus ( not n < F_{2}() - 1 implies y = 0 )
by A3; :: thesis: verum

end;then n + 1 < F

then consider y being set such that

A4: P

take y ; :: thesis: S

thus ( n < F

thus ( not n < F

A5: ( dom f = NAT & f . 0 = F

defpred S

$2 = f . (r - 1);

A6: for x being object st x in REAL holds

ex y being object st S

proof

consider g being Function such that
let x be object ; :: thesis: ( x in REAL implies ex y being object st S_{2}[x,y] )

assume x in REAL ; :: thesis: ex y being object st S_{2}[x,y]

then reconsider r = x as Real ;

take f . (r - 1) ; :: thesis: S_{2}[x,f . (r - 1)]

thus S_{2}[x,f . (r - 1)]
; :: thesis: verum

end;assume x in REAL ; :: thesis: ex y being object st S

then reconsider r = x as Real ;

take f . (r - 1) ; :: thesis: S

thus S

A7: ( dom g = REAL & ( for x being object st x in REAL holds

S

Seg F

then A8: dom (g | (Seg F

then reconsider p = g | (Seg F

take p ; :: thesis: ( len p = F

P

F

hence len p = F

P

( not F

proof

hence
( p . 1 = F
assume
F_{2}() <> 0
; :: thesis: ( p . 1 = F_{1}() or F_{2}() = 0 )

then consider k being Nat such that

A9: F_{2}() = k + 1
by NAT_1:6;

0 + 1 <= k + 1 by XREAL_1:7;

then 1 in Seg F_{2}()
by A9, FINSEQ_1:1;

then p . 1 = g . 1 by FUNCT_1:49

.= f . (1 - 1) by A7, Lm2

.= F_{1}()
by A5
;

hence ( p . 1 = F_{1}() or F_{2}() = 0 )
; :: thesis: verum

end;then consider k being Nat such that

A9: F

0 + 1 <= k + 1 by XREAL_1:7;

then 1 in Seg F

then p . 1 = g . 1 by FUNCT_1:49

.= f . (1 - 1) by A7, Lm2

.= F

hence ( p . 1 = F

P

let n be Nat; :: thesis: ( 1 <= n & n < F

assume that

A10: 1 <= n and

A11: n < F

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 < F

p . (n + 1) = f . n

proof

reconsider k = k as Nat ;
let n be Nat; :: thesis: ( n < F_{2}() implies p . (n + 1) = f . n )

assume n < F_{2}()
; :: thesis: p . (n + 1) = f . n

then ( 1 <= n + 1 & n + 1 <= F_{2}() )
by NAT_1:11, NAT_1:13;

then A14: n + 1 in Seg F_{2}()
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;assume n < F

then ( 1 <= n + 1 & n + 1 <= F

then A14: n + 1 in Seg F

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

k <= k + 1 by NAT_1:11;

then A15: k < F

k < F

then P

then P

hence P