(len (1_. L)) -' 1 = 1 -' 1 by POLYNOM4:4
.= 0 by XREAL_1:232 ;
then LC (1_. L) = 1. L by POLYNOM3:30;
hence 1_. L is monic by RATFUNC1:def 7; :: thesis: verum