theorem Th6: :: HOLDER_1:6

for p, q being Real st 1 < p & (1 / p) + (1 / q) = 1 holds
for a, b, ap, bq, ab being Real_Sequence st ( for n being Nat holds
( ap . n = |.(a . n).| to_power p & bq . n = |.(b . n).| to_power q & ab . n = |.((a . n) * (b . n)).| ) ) holds
for n being Nat holds (Partial_Sums ab) . n <= (((Partial_Sums ap) . n) to_power (1 / p)) * (((Partial_Sums bq) . n) to_power (1 / q))