let s be Real_Sequence; :: thesis: ( ( for n being Element of NAT holds
( s . n > - 1 & 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 > - 1 & 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
defpred S₁[ Element of NAT ] means ((Partial_Sums s) . $1) * (s . ($1 + 1)) >= 0 ;
A2: ((Partial_Sums s) . 0 ) * (s . 1) = (s . 0 ) * (s . 1) by SERIES_1:def 1;
( s . 0 < 0 & s . 1 < 0 ) by A1;
then A3: S₁[ 0 ] by A2;
A4: for n being Element of NAT st S₁[n] holds
S₁[n + 1]

proof

let n be Element of NAT ; :: thesis: ( S₁[n] implies S₁[n + 1] )
assume A5: ((Partial_Sums s) . n) * (s . (n + 1)) >= 0 ; :: thesis: S₁[n + 1]
A6: s . (n + 1) < 0 by A1;
then 1 / (s . (n + 1)) < 0 / (s . (n + 1)) ;
then (((Partial_Sums s) . n) * (s . (n + 1))) * (1 / (s . (n + 1))) <= 0 * (1 / (s . (n + 1))) by A5;
then ((Partial_Sums s) . n) * ((s . (n + 1)) * (1 / (s . (n + 1)))) <= 0 ;
then A7: ((Partial_Sums s) . n) * 1 <= 0 by A6;
A8: ((Partial_Sums s) . (n + 1)) * (s . (n + 2)) = (((Partial_Sums s) . n) + (s . (n + 1))) * (s . (n + 2)) by SERIES_1:def 1
.= (((Partial_Sums s) . n) * (s . (n + 2))) + ((s . (n + 1)) * (s . (n + 2))) ;
A9: ( s . (n + 2) <= 0 & s . (n + 1) <= 0 ) by A1;
then A10: ((Partial_Sums s) . n) * (s . (n + 2)) >= 0 by A7;
(s . (n + 1)) * (s . (n + 2)) >= 0 by A9;
then (((Partial_Sums s) . n) * (s . (n + 2))) + ((s . (n + 1)) * (s . (n + 2))) >= 0 + 0 by A10;
hence S₁[n + 1] by A8; :: thesis: verum

end;

for n being Element of NAT holds S₁[n] from NAT_1:sch 1(A3, A4);
hence ((Partial_Sums s) . n) * (s . (n + 1)) >= 0 ; :: thesis: verum