defpred S₁[ 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 ) );

A1: now :: thesis: for k being Nat st S₁[k] holds
S₁[k + 1]

let k be Nat; :: thesis: ( S₁[k] implies S₁[k + 1] )
assume A2: S₁[k] ; :: thesis: S₁[k + 1]

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

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

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 16;
x = x | (k + 1) by A5, FINSEQ_1:58
.= x | (Seg (k + 1)) by FINSEQ_1:def 16
.= 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

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 16; :: thesis: verum

end;

A12: k + 1 in Seg (k + 1) by FINSEQ_1:4;

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

let i be Nat; :: thesis: ( i in Seg (k + 1) implies x . b₁ <= Sum x )
assume A14: i in Seg (k + 1) ; :: thesis: x . b₁ <= Sum x
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;

suppose i < k + 1 ; :: thesis: x . b₁ <= 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;

suppose i = k + 1 ; :: thesis: x . b₁ <= Sum x

hence x . i <= Sum x by A2, A10, A9, XREAL_1:31; :: thesis: verum

end;

end;

end;

0 <= Sum xk by A2, A10;
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;

end;

hence S₁[k + 1] ; :: thesis: verum

end;

A19: S₁[ 0 ] by RVSUM_1:72;
thus for k being Nat holds S₁[k] from NAT_1:sch 2(A19, A1); :: thesis: verum