theorem :: HOLDER_1:12

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)).| ) ) & ap is summable & bq is summable holds
( ab is summable & Sum ab <= ((Sum ap) to_power (1 / p)) * ((Sum bq) to_power (1 / q)) )