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