set X0 = { the carrier of (REAL-NS (k . i)) where i is Nat : ( 1 <= i & i <= (len N) + 1 ) } ;
( 1 <= 1 & 1 <= (len N) + 1 )
by NAT_1:11;
then
the carrier of (REAL-NS (k . 1)) in { the carrier of (REAL-NS (k . i)) where i is Nat : ( 1 <= i & i <= (len N) + 1 ) }
;
then reconsider X = union { the carrier of (REAL-NS (k . i)) where i is Nat : ( 1 <= i & i <= (len N) + 1 ) } as non empty set by TARSKI:def 4;
defpred S1[ Nat, object , object ] means ex pp being PartFunc of X,X ex NN being Function of (REAL-NS (k . ($1 + 1))),(REAL-NS (k . ($1 + 2))) st
( pp = $2 & NN = N . ($1 + 1) & $3 = NN * pp );
A3:
for i being Nat st 1 <= i & i < len N holds
for x being Element of PFuncs (X,X) ex y being Element of PFuncs (X,X) st S1[i,x,y]
proof
let i be
Nat;
( 1 <= i & i < len N implies for x being Element of PFuncs (X,X) ex y being Element of PFuncs (X,X) st S1[i,x,y] )
assume A4:
( 1
<= i &
i < len N )
;
for x being Element of PFuncs (X,X) ex y being Element of PFuncs (X,X) st S1[i,x,y]
let x be
Element of
PFuncs (
X,
X);
ex y being Element of PFuncs (X,X) st S1[i,x,y]
i + 1
<= len N
by A4, NAT_1:13;
then A5:
( 1
<= i + 1 &
i + 1
< len k )
by A1, NAT_1:13, NAT_1:11;
then
N . (i + 1) is
Function of
(REAL-NS (k . (i + 1))),
(REAL-NS (k . ((i + 1) + 1)))
by A1;
then reconsider NN =
N . (i + 1) as
Function of
(REAL-NS (k . (i + 1))),
(REAL-NS (k . (i + 2))) ;
the
carrier of
(REAL-NS (k . (i + 1))) in { the carrier of (REAL-NS (k . i)) where i is Nat : ( 1 <= i & i <= (len N) + 1 ) }
by A1, A5;
then A6:
the
carrier of
(REAL-NS (k . (i + 1))) c= X
by ZFMISC_1:74;
i + 1
<= (i + 1) + 1
by NAT_1:11;
then A7:
1
<= i + 2
by NAT_1:11;
(i + 1) + 1
<= len k
by NAT_1:13, A5;
then
the
carrier of
(REAL-NS (k . (i + 2))) in { the carrier of (REAL-NS (k . i)) where i is Nat : ( 1 <= i & i <= (len N) + 1 ) }
by A1, A7;
then
the
carrier of
(REAL-NS (k . (i + 2))) c= X
by ZFMISC_1:74;
then
(
dom NN c= X &
rng NN c= X )
by A6;
then
NN in PFuncs (
X,
X)
by PARTFUN1:def 3;
then reconsider NN =
NN as
PartFunc of
X,
X by PARTFUN1:46;
reconsider pp =
x as
PartFunc of
X,
X by PARTFUN1:46;
set y =
NN * pp;
reconsider y =
NN * pp as
Element of
PFuncs (
X,
X)
by PARTFUN1:45;
take
y
;
S1[i,x,y]
thus
S1[
i,
x,
y]
;
verum
end;
A9:
1 <= len N
by NAT_1:14, A2;
A10:
( 1 <= 1 & 1 < len k )
by A1, A2, NAT_1:13, NAT_1:14;
then reconsider N1 = N . 1 as Function of (REAL-NS (k . 1)),(REAL-NS (k . (1 + 1))) by A1;
the carrier of (REAL-NS (k . 1)) in { the carrier of (REAL-NS (k . i)) where i is Nat : ( 1 <= i & i <= (len N) + 1 ) }
by A10, A1;
then A11:
the carrier of (REAL-NS (k . 1)) c= X
by ZFMISC_1:74;
1 + 1 <= len k
by A10, NAT_1:13;
then
the carrier of (REAL-NS (k . 2)) in { the carrier of (REAL-NS (k . i)) where i is Nat : ( 1 <= i & i <= (len N) + 1 ) }
by A1;
then
the carrier of (REAL-NS (k . 2)) c= X
by ZFMISC_1:74;
then
( dom N1 c= X & rng N1 c= X )
by A11;
then reconsider N1 = N1 as Element of PFuncs (X,X) by PARTFUN1:def 3;
consider p being FinSequence of PFuncs (X,X) such that
A14:
len p = len N
and
A15:
( p . 1 = N1 or len N = 0 )
and
A16:
for i being Nat st 1 <= i & i < len N holds
S1[i,p . i,p . (i + 1)]
from RECDEF_1:sch 4(A3);
defpred S2[ Nat] means ( 1 <= $1 & $1 < len N implies ex NN being Function of (REAL-NS (k . ($1 + 1))),(REAL-NS (k . ($1 + 2))) ex pp being Function of (REAL-NS (k . 1)),(REAL-NS (k . ($1 + 1))) st
( NN = N . ($1 + 1) & pp = p . $1 & p . ($1 + 1) = NN * pp ) );
A17:
S2[ 0 ]
;
A18:
for i being Nat st S2[i] holds
S2[i + 1]
A25:
for i being Nat holds S2[i]
from NAT_1:sch 2(A17, A18);
p . (len N) is Function of (REAL-NS (k . 1)),(REAL-NS (k . (n + 1)))
proof
per cases
( 1 = len N or 1 <> len N )
;
suppose
1
<> len N
;
p . (len N) is Function of (REAL-NS (k . 1)),(REAL-NS (k . (n + 1)))then
1
< len N
by A9, XXREAL_0:1;
then A27:
1
+ 1
<= len N
by NAT_1:13;
reconsider i =
(len N) - 1 as
Nat by A9, INT_1:5, ORDINAL1:def 12;
A28:
(1 + 1) - 1
<= (len N) - 1
by A27, XREAL_1:9;
(len N) - 1
< (len N) - 0
by XREAL_1:15;
then consider NN being
Function of
(REAL-NS (k . (i + 1))),
(REAL-NS (k . (i + 2))),
pp being
Function of
(REAL-NS (k . 1)),
(REAL-NS (k . (i + 1))) such that A29:
(
NN = N . (i + 1) &
pp = p . i &
p . (i + 1) = NN * pp )
by A25, A28;
thus
p . (len N) is
Function of
(REAL-NS (k . 1)),
(REAL-NS (k . (n + 1)))
by A1, A29;
verum end;
end;
then reconsider F = p . (len N) as Function of (REAL-NS (k . 1)),(REAL-NS (k . (n + 1))) ;
take
F
; ex p being FinSequence st
( len p = len N & p . 1 = N . 1 & ( for i being Nat st 1 <= i & i < len N holds
ex NN being Function of (REAL-NS (k . (i + 1))),(REAL-NS (k . (i + 2))) ex pp being Function of (REAL-NS (k . 1)),(REAL-NS (k . (i + 1))) st
( NN = N . (i + 1) & pp = p . i & p . (i + 1) = NN * pp ) ) & F = p . (len N) )
thus
ex p being FinSequence st
( len p = len N & p . 1 = N . 1 & ( for i being Nat st 1 <= i & i < len N holds
ex NN being Function of (REAL-NS (k . (i + 1))),(REAL-NS (k . (i + 2))) ex pp being Function of (REAL-NS (k . 1)),(REAL-NS (k . (i + 1))) st
( NN = N . (i + 1) & pp = p . i & p . (i + 1) = NN * pp ) ) & F = p . (len N) )
by A2, A14, A15, A25; verum