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

proof

let i be Nat; :: thesis: ( S₁[i] implies S₁[i + 1] )
assume A3: S₁[i] ; :: thesis: S₁[i + 1]
A4: Px (a,((k + i) + 1)) = ((Px (a,(k + i))) * a) + ((Py (a,(k + i))) * ((a ^2) -' 1)) by Th9;
a >= 2 by NAT_2:29;
then a >= 1 by XXREAL_0:2;
then (Px (a,(k + i))) * a >= (Px (a,(k + i))) * 1 by XREAL_1:64;
then Px (a,((k + i) + 1)) >= ((Px (a,(k + i))) * 1) + 0 by A4, XREAL_1:7;
hence S₁[i + 1] by A3, XXREAL_0:2; :: thesis: verum

end;

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