theorem :: SERIES_5:53

for s, s1 being Real_Sequence st ( for n being Nat holds
( s . n > 0 & s1 . n = 1 / (s . n) ) ) holds
for n being Nat holds ((Partial_Sums s) . n) * ((Partial_Sums s1) . n) >= (n + 1) ^2