let L be domRing; :: thesis: for n being Element of NAT
for p being Polynomial of L st p <> 0_. L holds
p `^ n <> 0_. L
let n be Element of NAT ; :: thesis: for p being Polynomial of L st p <> 0_. L holds
p `^ n <> 0_. L
let p be Polynomial of L; :: thesis: ( p <> 0_. L implies p `^ n <> 0_. L )
defpred S<sub>1</sub>[ Element of NAT ] means p `^ $1 <> 0_. L;
assume A1: p <> 0_. L ; :: thesis: p `^ n <> 0_. L
A2: for n being Element of NAT st S₁[n] holds
S₁[n + 1]

proof

let n be Element of NAT ; :: thesis: ( S₁[n] implies S₁[n + 1] )
assume A3: S₁[n] ; :: thesis: S₁[n + 1]
p `^ (n + 1) = (p `^ n) *' p by POLYNOM5:19;
hence S₁[n + 1] by A1, A3, Th23; :: thesis: verum

end;

( (1_. L) . 0 = 1. L & (0_. L) . 0 = 0. L ) by FUNCOP_1:7, POLYNOM3:30;
then A4: S₁[ 0 ] by POLYNOM5:15;
for n being Element of NAT holds S₁[n] from NAT_1:sch 1(A4, A2);
hence p `^ n <> 0_. L ; :: thesis: verum