let s be Real_Sequence; :: thesis: ( ( for n being Nat holds
( s . n > - 1 & s . n < 0 ) ) implies for n being Nat holds ((Partial_Sums s) . n) * (s . (n + 1)) >= 0 )
defpred S₁[ Nat] means ((Partial_Sums s) . $1) * (s . ($1 + 1)) >= 0 ;
A1: ((Partial_Sums s) . 0) * (s . 1) = (s . 0) * (s . 1) by SERIES_1:def 1;
assume A2: for n being Nat holds
( s . n > - 1 & s . n < 0 ) ; :: thesis: for n being Nat holds ((Partial_Sums s) . n) * (s . (n + 1)) >= 0
A3: for n being Nat st S₁[n] holds
S₁[n + 1]

proof

let n be Nat; :: thesis: ( S₁[n] implies S₁[n + 1] )
assume A4: ((Partial_Sums s) . n) * (s . (n + 1)) >= 0 ; :: thesis: S₁[n + 1]
s . (n + 1) < 0 by A2;
then A5: ((Partial_Sums s) . n) * 1 <= 0 by A4;
A6: ((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))) ;
( s . (n + 2) <= 0 & s . (n + 1) <= 0 ) by A2;
hence S₁[n + 1] by A5, A6; :: thesis: verum

end;

let n be Nat; :: thesis: ((Partial_Sums s) . n) * (s . (n + 1)) >= 0
( s . 0 < 0 & s . 1 < 0 ) by A2;
then A7: S₁[ 0 ] by A1;
for n being Nat holds S₁[n] from NAT_1:sch 2(A7, A3);
hence ((Partial_Sums s) . n) * (s . (n + 1)) >= 0 ; :: thesis: verum