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 S1[ Nat] means p `^ $1 <> 0_. L;
assume A1: p <> 0_. L ; :: thesis: p `^ n <> 0_. L
A2: for n being Nat st S1[n] holds
S1[n + 1]
proof
let n be Nat; :: thesis: ( S1[n] implies S1[n + 1] )
assume A3: S1[n] ; :: thesis: S1[n + 1]
p `^ (n + 1) = (p `^ n) *' p by POLYNOM5:19;
hence S1[n + 1] by A1, A3, Th18; :: thesis: verum
end;
( (1_. L) . 0 = 1. L & (0_. L) . 0 = 0. L ) by FUNCOP_1:7, POLYNOM3:30;
then A4: S1[ 0 ] by POLYNOM5:15;
for n being Nat holds S1[n] from NAT_1:sch 2(A4, A2);
 hence p `^ n <> 0_. L ; :: thesis: verum