len (1_. L) = 1 by POLYNOM4:4;
then (len (1_. L)) -' 1 = 1 - 1 by XREAL_0:def 2;
then LC (1_. L) = 1. L by POLYNOM3:30;
then [(1_. L),(1_. L)] `2 is normalized ;
hence 1._ L is normalized ; :: thesis: verum