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 )
assume A1: p <> 0_. L ; :: thesis: p `^ n <> 0_. L
A2: ( (1_. L) . 0 = 1. L & (0_. L) . 0 = 0. L ) by FUNCOP_1:13, POLYNOM3:31;
defpred S₁[ Element of NAT ] means p `^ $1 <> 0_. L;
A3: S₁[ 0 ] by A2, POLYNOM5:16;
A4: 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 A5: S₁[n] ; :: thesis: S₁[n + 1]
p `^ (n + 1) = (p `^ n) *' p by POLYNOM5:20;
hence S₁[n + 1] by A1, A5, Th23; :: thesis: verum

end;

for n being Element of NAT holds S₁[n] from NAT_1:sch 1(A3, A4);
hence p `^ n <> 0_. L ; :: thesis: verum