reconsider p1 = p as Polynomial of F ;
deg p1 > 0 by RING_4:def 4;
then reconsider p1 = p1 as non constant Polynomial of F by RATFUNC1:def 2;
defpred S₁[ Nat] means not p |^ F is constant ;
IA: S₁[1] by BINOM:8;

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 S₁[k] ; :: thesis: S₁[k + 1]
p |^ (k + 1) = (p |^ k) * (p |^ 1) by BINOM:10
.= (p |^ k) * p by BINOM:8
.= (p `^ k) *' p by POLYNOM3:def 10 ;
then ( p1 `^ (k + 1) = (p1 `^ k) *' p & p1 <> 0_. F & p1 `^ k <> 0_. F ) ;
then deg (p1 `^ (k + 1)) = (deg (p1 `^ k)) + (deg p) by HURWITZ:23;
hence S₁[k + 1] by RATFUNC1:def 2, RING_4:def 4; :: 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