let s be Real_Sequence; :: thesis: ( ( for n being Nat holds s . n >= 0 ) implies for n being Nat holds ((Partial_Sums s) . n) * (s . (n + 1)) >= 0 )
assume A1: for n being Nat holds s . n >= 0 ; :: thesis: for n being Nat holds ((Partial_Sums s) . n) * (s . (n + 1)) >= 0
let n be Nat; :: thesis: ((Partial_Sums s) . n) * (s . (n + 1)) >= 0
( (Partial_Sums s) . n >= 0 & s . (n + 1) >= 0 ) by A1, Th34;
hence ((Partial_Sums s) . n) * (s . (n + 1)) >= 0 ; :: thesis: verum