let a, b, c, k, n be Nat; :: thesis: ( c |^ n > (a |^ n) + (b |^ n) implies c |^ (k + n) > (a |^ (k + n)) + (b |^ (k + n)) )
assume AX: c |^ n > (a |^ n) + (b |^ n) ; :: thesis: c |^ (k + n) > (a |^ (k + n)) + (b |^ (k + n))
then n <> 0 by Lm0;
then consider m being Nat such that
AY: n = 1 + m by NAT_1:10, NAT_1:14;
defpred S₁[ Nat] means c |^ (($1 + m) + 1) > (a |^ (($1 + m) + 1)) + (b |^ (($1 + m) + 1));
A1: S₁[ 0 ] by AX, AY;
A2: for x being Nat st S₁[x] holds
S₁[x + 1] by Lm29;
for j being Nat holds S₁[j] from NAT_1:sch 2(A1, A2);
then c |^ ((k + m) + 1) > (a |^ ((k + m) + 1)) + (b |^ ((k + m) + 1)) ;
hence c |^ (k + n) > (a |^ (k + n)) + (b |^ (k + n)) by AY; :: thesis: verum