let R be domRing; :: thesis: for p being non zero Polynomial of R
for n being Nat holds deg (p `^ n) = n * (deg p)
let p be non zero Polynomial of R; :: thesis: for n being Nat holds deg (p `^ n) = n * (deg p)
let n be Nat; :: thesis: deg (p `^ n) = n * (deg p)
defpred S<sub>1</sub>[ Nat] means deg (p `^ $1) = $1 * (deg p);
H1: 1. R <> 0. R ;
deg (p `^ 0) = deg (1_. R) by POLYNOM5:15
.= deg ((1. R) | R) by RING_4:14
.= 0 * (deg p) by H1, RING_4:21 ;
then IA: S₁[ 0 ] ;

IS: now :: thesis: for k being Nat st S₁[k] holds
S₁[k + 1]

let k be Nat; :: thesis: ( S₁[k] implies S₁[k + 1] )
assume IV: S₁[k] ; :: thesis: S₁[k + 1]
H2: ( p <> 0_. R & p `^ k <> 0_. R ) ;
deg (p `^ (k + 1)) = deg ((p `^ k) *' p) by POLYNOM5:19
.= (deg (p `^ k)) + (deg p) by H2, HURWITZ:23
.= (k + 1) * (deg p) by IV ;
hence S₁[k + 1] ; :: thesis: verum

end;

for k being Nat holds S₁[k] from NAT_1:sch 2(IA, IS);
hence deg (p `^ n) = n * (deg p) ; :: thesis: verum