defpred S₁[ 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: S₁[ 0 ]

proof

let d be XFinSequence of REAL ; :: thesis: ( len d = 0 & ( 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 = 0 & ( for i being Nat st i in dom d holds
0 <= d . i ) ) ; :: thesis: ex M being Real st
( 0 <= M & ( for i being Nat st i in dom d holds
d . i <= M ) )
set M = 0 ;
take 0 ; :: thesis: ( 0 <= 0 & ( for i being Nat st i in dom d holds
d . i <= 0 ) )
thus 0 <= 0 ; :: thesis: for i being Nat st i in dom d holds
d . i <= 0
thus for i being Nat st i in dom d holds
d . i <= 0 by A1; :: thesis: verum

end;

P1: for k being Nat st S₁[k] holds
S₁[k + 1]

proof

let k be Nat; :: thesis: ( S₁[k] implies S₁[k + 1] )
assume A0: S₁[k] ; :: thesis: S₁[k + 1]
let d be XFinSequence of REAL ; :: thesis: ( 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 ) ) ; :: thesis: 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

proof

let i be Nat; :: thesis: ( i in dom d1 implies 0 <= d1 . i )
assume AA1: i in dom d1 ; :: thesis: 0 <= d1 . i
then AA2: d1 . i = d . i by A2, FUNCT_1:47;
k <= k + 1 by NAT_1:13;
then Segm k c= Segm (k + 1) by NAT_1:39;
hence 0 <= d1 . i by A1, AA2, AA1, A2; :: thesis: verum

end;

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 ; :: thesis: ( 0 <= M & ( for i being Nat st i in dom d holds
d . i <= M ) )
thus 0 <= M ; :: thesis: for i being Nat st i in dom d holds
d . i <= M
let i be Nat; :: thesis: ( i in dom d implies d . i <= M )
assume i in dom d ; :: thesis: 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;

per cases ( i <> k or i = k ) ;

suppose i <> k ; :: thesis: d . i <= M

then i < k by XXREAL_0:1, Q6;
then Q8P: i in Segm k by NAT_1:44;
then Q9: d1 . i = d . i by A2, FUNCT_1:47;
d1 . i <= M0 by A3, Q8P, A2;
hence d . i <= M by Q9, Q2, XXREAL_0:2; :: thesis: verum

end;

suppose i = k ; :: thesis: d . i <= M

hence d . i <= M by Q2P, A2, Q1, XXREAL_0:2; :: thesis: verum

end;

end;

end;

X1: for k being Nat holds S₁[k] from NAT_1:sch 2(P0, P1);
let d be XFinSequence of REAL ; :: thesis: ( ( 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 ; :: thesis: 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; :: thesis: verum