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()
now :: thesis: for n being Nat holds (Partial_Sums s) . n <= (Partial_Sums s) . (n + 1)
let 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;
hence Partial_Sums s is V47() ; :: thesis: verum