theorem :: HOLDER_1:13

for p being Real st 1 < p holds
for a, b, ap, bp, ab being Real_Sequence st ( for n being Nat holds
( ap . n = |.(a . n).| to_power p & bp . n = |.(b . n).| to_power p & ab . n = |.((a . n) + (b . n)).| to_power p ) ) & ap is summable & bp is summable holds
( ab is summable & (Sum ab) to_power (1 / p) <= ((Sum ap) to_power (1 / p)) + ((Sum bp) to_power (1 / p)) )