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

proof

let n be Nat; :: thesis: ( S₁[n] implies S₁[n + 1] )
A3: ((Partial_Product s1) . n) * (1 + (s . (n + 1))) = ((Partial_Product s1) . n) * (s1 . (n + 1)) by A1;
s . (n + 1) > - 1 by A1;
then A4: (s . (n + 1)) + 1 > (- 1) + 1 by XREAL_1:8;
assume 1 + ((Partial_Sums s) . n) <= (Partial_Product s1) . n ; :: thesis: S₁[n + 1]
then (1 + ((Partial_Sums s) . n)) * (1 + (s . (n + 1))) <= ((Partial_Product s1) . n) * (1 + (s . (n + 1))) by A4, XREAL_1:64;
then A5: (1 + ((Partial_Sums s) . n)) * (1 + (s . (n + 1))) <= (Partial_Product s1) . (n + 1) by A3, Def1;
((Partial_Sums s) . n) * (s . (n + 1)) >= 0 by A1, Lm8;
then A6: (((Partial_Sums s) . n) * (s . (n + 1))) + ((1 + (s . (n + 1))) + ((Partial_Sums s) . n)) >= 0 + ((1 + (s . (n + 1))) + ((Partial_Sums s) . n)) by XREAL_1:6;
1 + ((Partial_Sums s) . (n + 1)) = 1 + (((Partial_Sums s) . n) + (s . (n + 1))) by SERIES_1:def 1;
hence S₁[n + 1] by A5, A6, XXREAL_0:2; :: thesis: verum

end;

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