a <> 0. L ;
then len (a * p) = len p by POLYNOM5:25;
then a * p <> 0_. L by POLYNOM4:3, POLYNOM4:5;
hence not a * p is zero ; :: thesis: verum