defpred S_{1}[ 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_{1}[ 0 ]
_{1}[k] holds

S_{1}[k + 1]
_{1}[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

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

proof

P1:
for k being Nat st S
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;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

S

proof

X1:
for k being Nat holds S
let k be Nat; :: thesis: ( S_{1}[k] implies S_{1}[k + 1] )

assume A0: S_{1}[k]
; :: thesis: S_{1}[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

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;

end;assume A0: S

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

then consider M0 being Real such that
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;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

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 )
;

end;

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

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