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