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_{1}[ Nat] means p `^ $1 <> 0_. L;

assume A1: p <> 0_. L ; :: thesis: p `^ n <> 0_. L

A2: for n being Nat st S_{1}[n] holds

S_{1}[n + 1]

then A4: S_{1}[ 0 ]
by POLYNOM5:15;

for n being Nat holds S_{1}[n]
from NAT_1:sch 2(A4, A2);

hence p `^ n <> 0_. L ; :: thesis: verum

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

assume A1: p <> 0_. L ; :: thesis: p `^ n <> 0_. L

A2: for n being Nat st S

S

proof

( (1_. L) . 0 = 1. L & (0_. L) . 0 = 0. L )
by FUNCOP_1:7, POLYNOM3:30;
let n be Nat; :: thesis: ( S_{1}[n] implies S_{1}[n + 1] )

assume A3: S_{1}[n]
; :: thesis: S_{1}[n + 1]

p `^ (n + 1) = (p `^ n) *' p by POLYNOM5:19;

hence S_{1}[n + 1]
by A1, A3, Th18; :: thesis: verum

end;assume A3: S

p `^ (n + 1) = (p `^ n) *' p by POLYNOM5:19;

hence S

then A4: S

for n being Nat holds S

hence p `^ n <> 0_. L ; :: thesis: verum