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;
defpred S₁[ Nat] means 0 <= (Partial_Sums seq) . $1;
assume A1: seq is nonnegative ; :: thesis: ( Partial_Sums seq is nonnegative & Partial_Sums seq is non-decreasing )
A2: for k being Nat st S₁[k] holds
S₁[k + 1]

proof

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

end;

(Partial_Sums seq) . 0 = seq . 0 by Def1;
then A5: S₁[ 0 ] by A1, SUPINF_2:51;
for m being Nat holds S₁[m] from NAT_1:sch 2(A5, A2);
then for k being object st k in dom (Partial_Sums seq) holds
0 <= (Partial_Sums seq) . k ;
hence Partial_Sums seq is nonnegative by SUPINF_2:52; :: thesis: Partial_Sums seq is non-decreasing
for n, m being Nat st m <= n holds
(Partial_Sums seq) . m <= (Partial_Sums seq) . n

proof

let n, m be Nat; :: thesis: ( m <= n implies (Partial_Sums seq) . m <= (Partial_Sums seq) . n )
reconsider m1 = m as Nat ;
defpred S₂[ Nat] means (Partial_Sums seq) . m1 <= (Partial_Sums seq) . $1;
A6: 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)
A7: 0 <= seq . (k + 1) by A1, SUPINF_2:51;
(Partial_Sums seq) . (k + 1) = ((Partial_Sums seq) . k) + (seq . (k + 1)) by Def1;
hence (Partial_Sums seq) . k <= (Partial_Sums seq) . (k + 1) by A7, XXREAL_3:39; :: thesis: verum

end;

A8: 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
A9: k >= m1 and
A10: for l being Nat st l >= m1 & l < k holds
S₂[l] ; :: thesis: S₂[k]

now :: thesis: ( k > m1 implies S₂[k] )

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

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

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

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

end;

suppose A12: 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 A13: k > l by XREAL_1:19;
k = l + 1 ;
then A14: (Partial_Sums seq) . l <= (Partial_Sums seq) . k by A6;
l >= m1 by A12, XREAL_1:19;
then (Partial_Sums seq) . m1 <= (Partial_Sums seq) . l by A10, A13;
hence S₂[k] by A14, XXREAL_0:2; :: thesis: verum

end;

end;

end;

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

end;

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

end;

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