len (LM p) = len p by POLYNOM4:15;
then LM p <> 0_. R by POLYNOM4:5, POLYNOM4:3;
hence not LM p is zero by UPROOTS:def 5; :: thesis: verum