set 00 = the Element of F_{1}();

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

A2: for n being Nat

for x being Element of F_{1}() ex y being Element of F_{1}() st S_{1}[n,x,y]
_{1}() such that

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

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

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

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

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

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

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

_{1}()
;

then reconsider p = p as FinSequence of F_{1}() by FINSEQ_1:def 4;

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

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

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

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

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

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

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

assume that

A17: 1 <= n and

A18: n <= F_{3}() - 1
; :: thesis: P_{1}[n,p /. n,p /. (n + 1)]

consider k being Nat such that

A19: n = k + 1 by A17, NAT_1:6;

A20: for n being Nat st n <= F_{3}() - 1 holds

p /. (n + 1) = f . n

k <= (F_{3}() - 1) - 1
by A18, A19, XREAL_1:19;

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

then P_{1}[k + 1,f . k,p /. ((k + 1) + 1)]
by A20, A18, A19;

hence P_{1}[n,p /. n,p /. (n + 1)]
by A20, A18, A19, A24, XXREAL_0:2; :: thesis: verum

defpred S

A2: for n being Nat

for x being Element of F

proof

consider f being sequence of F
let n be Nat; :: thesis: for x being Element of F_{1}() ex y being Element of F_{1}() st S_{1}[n,x,y]

let x be Element of F_{1}(); :: thesis: ex y being Element of F_{1}() st S_{1}[n,x,y]

( 0 <= n & n <= F_{3}() - 2 implies ex y being Element of F_{1}() st S_{1}[n,x,y] )
_{1}() st S_{1}[n,x,y]
; :: thesis: verum

end;let x be Element of F

( 0 <= n & n <= F

proof

hence
ex y being Element of F
A3:
0 + 1 <= n + 1
by XREAL_1:6;

assume that

0 <= n and

A4: n <= F_{3}() - 2
; :: thesis: ex y being Element of F_{1}() st S_{1}[n,x,y]

n + 1 <= (F_{3}() - 2) + 1
by A4, XREAL_1:6;

then consider y being Element of F_{1}() such that

A5: P_{1}[n + 1,x,y]
by A1, A3;

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

thus ( 0 <= n & n <= F_{3}() - 2 implies P_{1}[n + 1,x,y] )
by A5; :: thesis: ( ( not 0 <= n or not n <= F_{3}() - 2 ) implies y = the Element of F_{1}() )

thus ( ( not 0 <= n or not n <= F_{3}() - 2 ) implies y = the Element of F_{1}() )
by A4; :: thesis: verum

end;assume that

0 <= n and

A4: n <= F

n + 1 <= (F

then consider y being Element of F

A5: P

take y ; :: thesis: S

thus ( 0 <= n & n <= F

thus ( ( not 0 <= n or not n <= F

A6: ( f . 0 = F

defpred S

$2 = f . (r - 1);

A7: 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

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

S

Seg F

then A9: dom (g | (Seg F

then reconsider p = g | (Seg F

now :: thesis: for x being object st x in rng p holds

x in F_{1}()

then
rng p c= Fx in F

let x be object ; :: thesis: ( x in rng p implies x in F_{1}() )

assume x in rng p ; :: thesis: x in F_{1}()

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 F_{1}()

p . y = g . y by A10, FUNCT_1:47;

hence x in F_{1}()
by A8, A11, A12, A14; :: thesis: verum

end;assume x in rng p ; :: thesis: x in F

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 F

proof

A14:
y in REAL
by XREAL_0:def 1;
y <> 0
by A9, A10, FINSEQ_1:1;

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 F_{1}()
;

hence f . (y - 1) in F_{1}()
by A13; :: thesis: verum

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

hence f . (y - 1) in F

p . y = g . y by A10, FUNCT_1:47;

hence x in F

then reconsider p = p as FinSequence of F

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

P

thus len p = F

P

( F

proof

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

then consider k being Nat such that

A15: F_{3}() = k + 1
by NAT_1:6;

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

then A16: 1 in Seg F_{3}()
by A15, FINSEQ_1:1;

then p /. 1 = p . 1 by A9, PARTFUN1:def 6

.= g . 1 by A16, FUNCT_1:49

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

.= F_{2}()
by A6
;

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

end;then consider k being Nat such that

A15: F

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

then A16: 1 in Seg F

then p /. 1 = p . 1 by A9, PARTFUN1:def 6

.= g . 1 by A16, FUNCT_1:49

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

.= F

hence p /. 1 = F

P

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

assume that

A17: 1 <= n and

A18: n <= F

consider k being Nat such that

A19: n = k + 1 by A17, NAT_1:6;

A20: for n being Nat st n <= F

p /. (n + 1) = f . n

proof

A24:
k <= k + 1
by NAT_1:11;
let n be Nat; :: thesis: ( n <= F_{3}() - 1 implies p /. (n + 1) = f . n )

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

then A21: n + 1 <= (F_{3}() - 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 F_{3}()
by A21, FINSEQ_1:1;

then p /. (n + 1) = p . (n + 1) by A9, PARTFUN1:def 6;

hence p /. (n + 1) = f . n by A23, A22, FUNCT_1:49; :: thesis: verum

end;assume n <= F

then A21: n + 1 <= (F

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 F

then p /. (n + 1) = p . (n + 1) by A9, PARTFUN1:def 6;

hence p /. (n + 1) = f . n by A23, A22, FUNCT_1:49; :: thesis: verum

k <= (F

then P

then P

hence P