defpred S₁[ Nat] means not p `^ F is constant ;
IA: S₁[1] by POLYNOM5:16;

IS: now :: thesis: for k being Nat st k >= 1 & S₁[k] holds
S₁[k + 1]

let k be Nat; :: thesis: ( k >= 1 & S₁[k] implies S₁[k + 1] )
assume k >= 1 ; :: thesis: ( S₁[k] implies S₁[k + 1] )
assume IV: S₁[k] ; :: thesis: S₁[k + 1]
( p `^ (k + 1) = (p `^ k) *' p & p <> 0_. F & p `^ k <> 0_. F ) by POLYNOM5:19;
then H4: deg (p `^ (k + 1)) = (deg (p `^ k)) + (deg p) by HURWITZ:23;
( deg (p `^ k) > 0 & deg p > 0 ) by IV, RATFUNC1:def 2;
hence S₁[k + 1] by H4, RATFUNC1:def 2; :: thesis: verum

end;

I: for k being Nat st k >= 1 holds
S₁[k] from NAT_1:sch 8(IA, IS);
n >= 0 + 1 by INT_1:7;
hence not p `^ n is constant by I; :: thesis: verum