theorem :: MOEBIUS3:68

for n being Nat holds (Partial_Sums (rseq (0,1,1,0))) . n <= ((Partial_Sums Reci-Sqf) . n) * ((Partial_Sums Reci-TSq) . n) by SERIES_3:39, Seqs1, Seqs4, Core1;