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

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