defpred S1[ 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 S1[k] holds
S1[k + 1]
let k be Nat; :: thesis: ( S1[k] implies S1[k + 1] )
assume A2: S1[k] ; :: thesis: S1[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 ;
A5: k + 1 = len x by CARD_1:def 7;
then len (x | k) = k by ;
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 ;
then A7: k + 1 in dom x by FINSEQ_1:def 3;
reconsider xk = x | k as Element of REAL k by ;
A8: xk = x | (Seg k) by FINSEQ_1:def 15;
x = x | (k + 1) by
.= x | (Seg (k + 1)) by FINSEQ_1:def 15
.= xk ^ <*(x . (k + 1))*> by ;
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 ;
then 0 <= (x | (Seg k)) . i by ;
hence 0 <= xk . i by FINSEQ_1:def 15; :: 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 . b1 <= Sum x )
assume A14: i in Seg (k + 1) ; :: thesis: x . b1 <= Sum x
then A15: 1 <= i by FINSEQ_1:1;
A16: i <= k + 1 by ;
per cases ( i < k + 1 or i = k + 1 ) by ;
suppose i < k + 1 ; :: thesis: x . b1 <= Sum x
then i <= k by NAT_1:13;
then A17: i in Seg k by ;
then xk . i <= Sum xk by ;
then A18: x . i <= Sum xk by ;
Sum xk <= (Sum xk) + (x . (k + 1)) by ;
hence x . i <= Sum x by ; :: thesis: verum
end;
suppose i = k + 1 ; :: thesis: x . b1 <= Sum x
hence x . i <= Sum x by ; :: thesis: verum
end;
end;
end;
0 <= Sum xk by ;
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 S1[k + 1] ; :: thesis: verum
end;
A19: S1[ 0 ] by RVSUM_1:72;
thus for k being Nat holds S1[k] from NAT_1:sch 2(A19, A1); :: thesis: verum