let seq be ExtREAL_sequence; :: thesis: ( seq is nonnegative implies ( Partial_Sums seq is nonnegative & Partial_Sums seq is non-decreasing ) )
set PS = Partial_Sums seq;
assume A1: seq is nonnegative ; :: thesis: ( Partial_Sums seq is nonnegative & Partial_Sums seq is non-decreasing )
defpred S₁[ Nat] means 0 <= (Partial_Sums seq) . $1;
(Partial_Sums seq) . 0 = seq . 0 by Def1;
then A2: S₁[ 0 ] by A1, SUPINF_2:70;
A3: for k being Nat st S₁[k] holds
S₁[k + 1]

proof

let k be Nat; :: thesis: ( S₁[k] implies S₁[k + 1] )
assume A4: S₁[k] ; :: thesis: S₁[k + 1]
A5: seq . (k + 1) >= 0 by A1, SUPINF_2:70;
(Partial_Sums seq) . (k + 1) = ((Partial_Sums seq) . k) + (seq . (k + 1)) by Def1;
hence (Partial_Sums seq) . (k + 1) >= 0 by A4, A5, SUPINF_2:20; :: thesis: verum

end;

A6: for m being Nat holds S₁[m] from NAT_1:sch 2(A2, A3);
for k being set st k in dom (Partial_Sums seq) holds
0 <= (Partial_Sums seq) . k by A6;
hence Partial_Sums seq is nonnegative by SUPINF_2:71; :: thesis: Partial_Sums seq is non-decreasing
for n, m being Element of NAT st m <= n holds
(Partial_Sums seq) . m <= (Partial_Sums seq) . n

proof

let n, m be Element of NAT ; :: thesis: ( m <= n implies (Partial_Sums seq) . m <= (Partial_Sums seq) . n )
reconsider n1 = n, m1 = m as Nat ;
assume A7: m <= n ; :: thesis: (Partial_Sums seq) . m <= (Partial_Sums seq) . n
defpred S₂[ Nat] means (Partial_Sums seq) . m1 <= (Partial_Sums seq) . $1;
A8: for k being Nat holds (Partial_Sums seq) . k <= (Partial_Sums seq) . (k + 1)

proof

let k be Nat; :: thesis: (Partial_Sums seq) . k <= (Partial_Sums seq) . (k + 1)
A9: (Partial_Sums seq) . (k + 1) = ((Partial_Sums seq) . k) + (seq . (k + 1)) by Def1;
( 0 <= seq . (k + 1) & 0 <= (Partial_Sums seq) . k ) by A1, A6, SUPINF_2:70;
hence (Partial_Sums seq) . k <= (Partial_Sums seq) . (k + 1) by A9, SUPINF_2:20; :: thesis: verum

end;

A10: for k being Nat st k >= m1 & ( for l being Nat st l >= m1 & l < k holds
S₂[l] ) holds
S₂[k]

proof

let k be Nat; :: thesis: ( k >= m1 & ( for l being Nat st l >= m1 & l < k holds
S₂[l] ) implies S₂[k] )
assume that
A11: k >= m1 and
A12: for l being Nat st l >= m1 & l < k holds
S₂[l] ; :: thesis: S₂[k]

now

assume k > m1 ; :: thesis: S₂[k]
then A13: k >= m1 + 1 by NAT_1:13;

per cases ( k = m1 + 1 or k > m1 + 1 ) by A13, XXREAL_0:1;

suppose k = m1 + 1 ; :: thesis: S₂[k]

hence S₂[k] by A8; :: thesis: verum

end;

suppose A14: k > m1 + 1 ; :: thesis: S₂[k]

then reconsider l = k - 1 as Element of NAT by NAT_1:20;
k < k + 1 by NAT_1:13;
then ( k > l & l >= m1 ) by A14, XREAL_1:21;
then A15: (Partial_Sums seq) . m1 <= (Partial_Sums seq) . l by A12;
k = l + 1 ;
then (Partial_Sums seq) . l <= (Partial_Sums seq) . k by A8;
hence S₂[k] by A15, XXREAL_0:2; :: thesis: verum

end;

end;

end;

hence S₂[k] by A11, XXREAL_0:1; :: thesis: verum

end;

for k being Nat st k >= m1 holds
S₂[k] from NAT_1:sch 9(A10);
hence (Partial_Sums seq) . m <= (Partial_Sums seq) . n by A7; :: thesis: verum

end;

hence Partial_Sums seq is non-decreasing by RINFSUP2:7; :: thesis: verum