let a, b, c, k, m be Nat; :: thesis: ( c |^ m >= (a |^ m) + (b |^ m) implies c |^ (k + m) >= (a |^ (k + m)) + (b |^ (k + m)) )
assume A0: c |^ m >= (a |^ m) + (b |^ m) ; :: thesis: c |^ (k + m) >= (a |^ (k + m)) + (b |^ (k + m))
then A0a: m <> 0 by Lm0;
A0c: ( k = 0 implies c |^ (k + m) >= (a |^ (k + m)) + (b |^ (k + m)) ) by A0;

per cases ( a = 0 or b = 0 or ( a > 0 & b > 0 ) ) ;

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

then A1: ( ( a |^ m = 0 or b |^ m = 0 ) & ( a |^ (k + m) = 0 or b |^ (k + m) = 0 ) ) by A0a, NAT_1:14, NEWTON:11;
then ( c >= a & c >= b ) by A0, A0a, NAT_1:14, PREPOWER:10;
hence c |^ (k + m) >= (a |^ (k + m)) + (b |^ (k + m)) by A1, Lm3a; :: thesis: verum

end;

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

hence c |^ (k + m) >= (a |^ (k + m)) + (b |^ (k + m)) by A0, A0c, Th18; :: thesis: verum

end;

end;