let a, b be positive Real; :: thesis: for n being positive heavy Real holds (a to_power n) + (b to_power n) < (a + b) to_power n
let n be positive heavy Real; :: thesis: (a to_power n) + (b to_power n) < (a + b) to_power n
reconsider m = n - 1 as positive Real ;
(a to_power 1) + (b to_power 1) = (a + b) to_power 1 ;
then (a to_power (1 + m)) + (b to_power (1 + m)) < (a + b) to_power (1 + m) by NEW;
hence (a to_power n) + (b to_power n) < (a + b) to_power n ; :: thesis: verum