theorem :: SERIES_5:46

for a, b being positive Real
for n, k being Nat st n >= 1 & k >= 1 holds
((a |^ k) + (b |^ k)) * ((a |^ n) + (b |^ n)) <= 2 * ((a |^ (k + n)) + (b |^ (k + n)))