per cases ( p is zero or not p is zero ) ;

suppose p is zero ; :: thesis: p |^ n is constant

then p = 0_. F by UPROOTS:def 5
.= 0. (Polynom-Ring F) by POLYNOM3:def 10 ;
hence p |^ n is constant ; :: thesis: verum

end;

suppose not p is zero ; :: thesis: p |^ n is constant

then ( deg p <= 0 & deg (p `^ n) = n * (deg p) ) by t1, RING_4:def 4;
hence p |^ n is constant by RING_4:def 4; :: thesis: verum

end;

end;