let L be domRing; :: thesis: for p being Polynomial of L
for a being non zero Element of L holds deg (a * p) = deg p
let p be Polynomial of L; :: thesis: for a being non zero Element of L holds deg (a * p) = deg p
let v be non zero Element of L; :: thesis: deg (v * p) = deg p
len (v * p) = len p by Th25a;
hence deg (v * p) = (len p) - 1 by HURWITZ:def 2
.= deg p by HURWITZ:def 2 ;
:: thesis: verum