let R be domRing; :: thesis: for p being non zero Polynomial of R holds deg (<%(0. R),(1. R)%> *' p) = (deg p) + 1
let p be non zero Polynomial of R; :: thesis: deg (<%(0. R),(1. R)%> *' p) = (deg p) + 1
B: len <%(0. R),(1. R)%> = 2 by POLYNOM5:40;
then A: <%(0. R),(1. R)%> <> 0_. R by POLYNOM4:3;
C: deg <%(0. R),(1. R)%> = 2 - 1 by B, HURWITZ:def 2;
thus deg (<%(0. R),(1. R)%> *' p) = (deg p) + 1 by C, A, HURWITZ:23; :: thesis: verum