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 A1: k < n ; :: thesis: Px (a,k) < Px (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 Px (a,k) < Px (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: Px (a,((k + i) + 1)) = ((Px (a,(k + i))) * a) + ((Py (a,(k + i))) * ((a ^2) -' 1)) by HILB10_1:6;
Px (a,(k + i)) >= Px (a,0) by HILB10_1:10;
then Px (a,(k + i)) >= 1 by HILB10_1:3;
then A7: (Px (a,(k + i))) + (Px (a,(k + i))) >= (Px (a,(k + i))) + 1 by XREAL_1:7;
(Px (a,(k + i))) * a >= (Px (a,(k + i))) * 2 by NAT_2:29, XREAL_1:64;
then Px (a,((k + i) + 1)) >= ((Px (a,(k + i))) * 2) + 0 by A6, XREAL_1:7;
then A8: Px (a,((k + i) + 1)) >= (Px (a,(k + i))) + 1 by A7, XXREAL_0:2;
then A9: Px (a,((k + i) + 1)) > Px (a,(k + i)) by NAT_1:13;

per cases ( i = 0 or i > 0 ) ;

suppose i = 0 ; :: thesis: S₁[i + 1]

hence S₁[i + 1] by A8, NAT_1:13; :: thesis: verum

end;

suppose i > 0 ; :: thesis: S₁[i + 1]

hence S₁[i + 1] by A5, A9, XXREAL_0:2; :: thesis: verum

end;

end;

end;

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