let s be Real_Sequence; :: thesis: ( ( for n being Nat holds 0 <= s . n ) implies Partial_Sums s is V47() )

assume A1: for n being Nat holds 0 <= s . n ; :: thesis: Partial_Sums s is V47()

assume A1: for n being Nat holds 0 <= s . n ; :: thesis: Partial_Sums s is V47()

now :: thesis: for n being Nat holds (Partial_Sums s) . n <= (Partial_Sums s) . (n + 1)

hence
Partial_Sums s is V47()
; :: thesis: verumlet n be Nat; :: thesis: (Partial_Sums s) . n <= (Partial_Sums s) . (n + 1)

0 <= s . (n + 1) by A1;

then 0 + ((Partial_Sums s) . n) <= (s . (n + 1)) + ((Partial_Sums s) . n) by XREAL_1:6;

hence (Partial_Sums s) . n <= (Partial_Sums s) . (n + 1) by Def1; :: thesis: verum

end;0 <= s . (n + 1) by A1;

then 0 + ((Partial_Sums s) . n) <= (s . (n + 1)) + ((Partial_Sums s) . n) by XREAL_1:6;

hence (Partial_Sums s) . n <= (Partial_Sums s) . (n + 1) by Def1; :: thesis: verum