defpred S1[ Nat] means for d being XFinSequence of REAL st len d = $1 & ( for i being Nat st i in dom d holds
0 <= d . i ) holds
ex M being Real st
( 0 <= M & ( for i being Nat st i in dom d holds
d . i <= M ) );
P0:
S1[ 0 ]
P1:
for k being Nat st S1[k] holds
S1[k + 1]
proof
let k be
Nat;
( S1[k] implies S1[k + 1] )
assume A0:
S1[
k]
;
S1[k + 1]
let d be
XFinSequence of
REAL ;
( len d = k + 1 & ( for i being Nat st i in dom d holds
0 <= d . i ) implies ex M being Real st
( 0 <= M & ( for i being Nat st i in dom d holds
d . i <= M ) ) )
assume A1:
(
len d = k + 1 & ( for
i being
Nat st
i in dom d holds
0 <= d . i ) )
;
ex M being Real st
( 0 <= M & ( for i being Nat st i in dom d holds
d . i <= M ) )
consider a being
Real,
d1 being
XFinSequence of
REAL such that A2:
(
len d1 = k &
d1 = d | k &
a = d . k &
d = d1 ^ <%a%> )
by A1, LMXFIN3;
for
i being
Nat st
i in dom d1 holds
0 <= d1 . i
then consider M0 being
Real such that A3:
(
0 <= M0 & ( for
i being
Nat st
i in dom d1 holds
d1 . i <= M0 ) )
by A0, A2;
set M =
[/(max (M0,a))\];
Q1:
(
M0 <= max (
M0,
a) &
a <= max (
M0,
a) )
by XXREAL_0:25;
Q2P:
max (
M0,
a)
<= [/(max (M0,a))\]
by INT_1:def 7;
then Q2:
(
M0 <= [/(max (M0,a))\] &
a <= [/(max (M0,a))\] )
by Q1, XXREAL_0:2;
[/(max (M0,a))\] in NAT
by INT_1:3, A3, Q1, Q2P;
then reconsider M =
[/(max (M0,a))\] as
Nat ;
take
M
;
( 0 <= M & ( for i being Nat st i in dom d holds
d . i <= M ) )
thus
0 <= M
;
for i being Nat st i in dom d holds
d . i <= M
let i be
Nat;
( i in dom d implies d . i <= M )
assume
i in dom d
;
d . i <= M
then
i in Segm (k + 1)
by A1;
then
i < k + 1
by NAT_1:44;
then Q6:
i <= k
by NAT_1:13;
end;
X1:
for k being Nat holds S1[k]
from NAT_1:sch 2(P0, P1);
let d be XFinSequence of REAL ; ( ( for i being Nat st i in dom d holds
0 <= d . i ) implies ex M being Real st
( 0 <= M & ( for i being Nat st i in dom d holds
d . i <= M ) ) )
assume X2:
for i being Nat st i in dom d holds
0 <= d . i
; ex M being Real st
( 0 <= M & ( for i being Nat st i in dom d holds
d . i <= M ) )
thus
ex M being Real st
( 0 <= M & ( for i being Nat st i in dom d holds
d . i <= M ) )
by X1, X2; verum