p <> 0_. L ;
then len p <> 0 by POLYNOM4:5;
then 0 + 1 < (len p) + 1 by XREAL_1:8;
then len p >= 1 by NAT_1:13;
then ((len p) -' 1) + 1 = len p by XREAL_1:235;
then p . ((len p) -' 1) <> 0. L by ALGSEQ_1:10;
hence not LC p is zero ; :: thesis: verum