let a, b, c, m be Nat; :: thesis: ( c |^ m > (a |^ m) + (b |^ m) & a > 0 implies c |^ (m + 1) > (a |^ (m + 1)) + (b |^ (m + 1)) )
assume A1: ( c |^ m > (a |^ m) + (b |^ m) & a > 0 ) ; :: thesis: c |^ (m + 1) > (a |^ (m + 1)) + (b |^ (m + 1))
then A2: m <> 0 by Lm0;

per cases ( b = 0 or b <> 0 ) ;

suppose b = 0 ; :: thesis: c |^ (m + 1) > (a |^ (m + 1)) + (b |^ (m + 1))

then ( b |^ m = 0 & b |^ (m + 1) = 0 ) by A2, NEWTON:84;
hence c |^ (m + 1) > (a |^ (m + 1)) + (b |^ (m + 1)) by A1, Lm4a; :: thesis: verum

end;

suppose b <> 0 ; :: thesis: c |^ (m + 1) > (a |^ (m + 1)) + (b |^ (m + 1))

hence c |^ (m + 1) > (a |^ (m + 1)) + (b |^ (m + 1)) by A1, Th18; :: thesis: verum

end;

end;