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 by defnormp;
hence 1._ L is normalized by defnorm; :: thesis: verum