let n, k be Nat; :: thesis: for a being non trivial Nat st k < n holds
Py (a,k) < Py (a,n)
let a be non trivial Nat; :: thesis: ( k < n implies Py (a,k) < Py (a,n) )
assume A1: k < n ; :: thesis: Py (a,k) < Py (a,n)
then reconsider nk = n - k as Nat by NAT_1:21;
A2: nk <> 0 by A1;
defpred S₁[ Nat] means ( $1 > 0 implies Py (a,k) < Py (a,(k + $1)) );
A3: S₁[ 0 ] ;
A4: for i being Nat st S₁[i] holds
S₁[i + 1]

proof

let i be Nat; :: thesis: ( S₁[i] implies S₁[i + 1] )
assume A5: S₁[i] ; :: thesis: S₁[i + 1]
A6: Py (a,((k + i) + 1)) = ((Py (a,(k + i))) * a) + (Px (a,(k + i))) by Th9;
a >= 2 by NAT_2:29;
then a >= 1 by XXREAL_0:2;
then (Py (a,(k + i))) * a >= (Py (a,(k + i))) * 1 by XREAL_1:64;
then A7: Py (a,((k + i) + 1)) > ((Py (a,(k + i))) * 1) + 0 by A6, XREAL_1:8;
( i = 0 or i > 0 ) ;
hence S₁[i + 1] by A7, A5, XXREAL_0:2; :: thesis: verum

end;

for n1 being Nat holds S₁[n1] from NAT_1:sch 2(A3, A4);
then S₁[nk] ;
hence Py (a,k) < Py (a,n) by A2; :: thesis: verum