defpred S_{1}[ Nat] means for x being Element of REAL $1 st ( for i being Nat st i in Seg $1 holds

0 <= x . i ) holds

( 0 <= Sum x & ( for i being Nat st i in Seg $1 holds

x . i <= Sum x ) );

_{1}[ 0 ]
by RVSUM_1:72;

thus for k being Nat holds S_{1}[k]
from NAT_1:sch 2(A19, A1); :: thesis: verum

0 <= x . i ) holds

( 0 <= Sum x & ( for i being Nat st i in Seg $1 holds

x . i <= Sum x ) );

A1: now :: thesis: for k being Nat st S_{1}[k] holds

S_{1}[k + 1]

A19:
SS

let k be Nat; :: thesis: ( S_{1}[k] implies S_{1}[k + 1] )

assume A2: S_{1}[k]
; :: thesis: S_{1}[k + 1]

_{1}[k + 1]
; :: thesis: verum

end;assume A2: S

now :: thesis: for x being Element of REAL (k + 1) st ( for i being Nat st i in Seg (k + 1) holds

0 <= x . i ) holds

( 0 <= Sum x & ( for i being Nat st i in Seg (k + 1) holds

x . i <= Sum x ) )

hence
S0 <= x . i ) holds

( 0 <= Sum x & ( for i being Nat st i in Seg (k + 1) holds

x . i <= Sum x ) )

let x be Element of REAL (k + 1); :: thesis: ( ( for i being Nat st i in Seg (k + 1) holds

0 <= x . i ) implies ( 0 <= Sum x & ( for i being Nat st i in Seg (k + 1) holds

x . i <= Sum x ) ) )

assume A3: for i being Nat st i in Seg (k + 1) holds

0 <= x . i ; :: thesis: ( 0 <= Sum x & ( for i being Nat st i in Seg (k + 1) holds

x . i <= Sum x ) )

thus ( 0 <= Sum x & ( for i being Nat st i in Seg (k + 1) holds

x . i <= Sum x ) ) :: thesis: verum

end;0 <= x . i ) implies ( 0 <= Sum x & ( for i being Nat st i in Seg (k + 1) holds

x . i <= Sum x ) ) )

assume A3: for i being Nat st i in Seg (k + 1) holds

0 <= x . i ; :: thesis: ( 0 <= Sum x & ( for i being Nat st i in Seg (k + 1) holds

x . i <= Sum x ) )

thus ( 0 <= Sum x & ( for i being Nat st i in Seg (k + 1) holds

x . i <= Sum x ) ) :: thesis: verum

proof

set xk = x | k;

A4: 0 <= x . (k + 1) by A3, FINSEQ_1:4;

A5: k + 1 = len x by CARD_1:def 7;

then len (x | k) = k by FINSEQ_1:59, NAT_1:11;

then A6: x | k is Element of k -tuples_on REAL by FINSEQ_2:92;

1 <= k + 1 by NAT_1:11;

then k + 1 in Seg (len x) by A5, FINSEQ_1:1;

then A7: k + 1 in dom x by FINSEQ_1:def 3;

reconsider xk = x | k as Element of REAL k by A6, EUCLID:def 1;

A8: xk = x | (Seg k) by FINSEQ_1:def 15;

x = x | (k + 1) by A5, FINSEQ_1:58

.= x | (Seg (k + 1)) by FINSEQ_1:def 15

.= xk ^ <*(x . (k + 1))*> by A7, A8, FINSEQ_5:10 ;

then A9: Sum x = (Sum xk) + (x . (k + 1)) by RVSUM_1:74;

hence ( 0 <= Sum x & ( for i being Nat st i in Seg (k + 1) holds

x . i <= Sum x ) ) by A4, A9, A13; :: thesis: verum

end;A4: 0 <= x . (k + 1) by A3, FINSEQ_1:4;

A5: k + 1 = len x by CARD_1:def 7;

then len (x | k) = k by FINSEQ_1:59, NAT_1:11;

then A6: x | k is Element of k -tuples_on REAL by FINSEQ_2:92;

1 <= k + 1 by NAT_1:11;

then k + 1 in Seg (len x) by A5, FINSEQ_1:1;

then A7: k + 1 in dom x by FINSEQ_1:def 3;

reconsider xk = x | k as Element of REAL k by A6, EUCLID:def 1;

A8: xk = x | (Seg k) by FINSEQ_1:def 15;

x = x | (k + 1) by A5, FINSEQ_1:58

.= x | (Seg (k + 1)) by FINSEQ_1:def 15

.= xk ^ <*(x . (k + 1))*> by A7, A8, FINSEQ_5:10 ;

then A9: Sum x = (Sum xk) + (x . (k + 1)) by RVSUM_1:74;

A10: now :: thesis: for i being Nat st i in Seg k holds

0 <= xk . i

A12:
k + 1 in Seg (k + 1)
by FINSEQ_1:4;0 <= xk . i

let i be Nat; :: thesis: ( i in Seg k implies 0 <= xk . i )

assume A11: i in Seg k ; :: thesis: 0 <= xk . i

k <= k + 1 by NAT_1:11;

then Seg k c= Seg (k + 1) by FINSEQ_1:5;

then 0 <= x . i by A3, A11;

then 0 <= (x | (Seg k)) . i by A11, FUNCT_1:49;

hence 0 <= xk . i by FINSEQ_1:def 15; :: thesis: verum

end;assume A11: i in Seg k ; :: thesis: 0 <= xk . i

k <= k + 1 by NAT_1:11;

then Seg k c= Seg (k + 1) by FINSEQ_1:5;

then 0 <= x . i by A3, A11;

then 0 <= (x | (Seg k)) . i by A11, FUNCT_1:49;

hence 0 <= xk . i by FINSEQ_1:def 15; :: thesis: verum

A13: now :: thesis: for i being Nat st i in Seg (k + 1) holds

x . i <= Sum x

0 <= Sum xk
by A2, A10;x . i <= Sum x

let i be Nat; :: thesis: ( i in Seg (k + 1) implies x . b_{1} <= Sum x )

assume A14: i in Seg (k + 1) ; :: thesis: x . b_{1} <= Sum x

then A15: 1 <= i by FINSEQ_1:1;

A16: i <= k + 1 by A14, FINSEQ_1:1;

end;assume A14: i in Seg (k + 1) ; :: thesis: x . b

then A15: 1 <= i by FINSEQ_1:1;

A16: i <= k + 1 by A14, FINSEQ_1:1;

per cases
( i < k + 1 or i = k + 1 )
by A16, XXREAL_0:1;

end;

suppose
i < k + 1
; :: thesis: x . b_{1} <= Sum x

then
i <= k
by NAT_1:13;

then A17: i in Seg k by A15, FINSEQ_1:1;

then xk . i <= Sum xk by A2, A10;

then A18: x . i <= Sum xk by A8, A17, FUNCT_1:49;

Sum xk <= (Sum xk) + (x . (k + 1)) by A3, A12, XREAL_1:31;

hence x . i <= Sum x by A9, A18, XXREAL_0:2; :: thesis: verum

end;then A17: i in Seg k by A15, FINSEQ_1:1;

then xk . i <= Sum xk by A2, A10;

then A18: x . i <= Sum xk by A8, A17, FUNCT_1:49;

Sum xk <= (Sum xk) + (x . (k + 1)) by A3, A12, XREAL_1:31;

hence x . i <= Sum x by A9, A18, XXREAL_0:2; :: thesis: verum

hence ( 0 <= Sum x & ( for i being Nat st i in Seg (k + 1) holds

x . i <= Sum x ) ) by A4, A9, A13; :: thesis: verum

thus for k being Nat holds S