A: LC p <> 0. L ;
LC (((1. L) / (LC p)) * p) = ((1. L) / (LC p)) * (LC p) by lcp1
.= (1. L) * (((LC p) ") * (LC p)) by GROUP_1:def 3
.= (1. L) * (1. L) by A, VECTSP_1:def 10
.= 1. L by VECTSP_1:def 4 ;
hence ((1. L) / (LC p)) * p is normalized by defnormp; :: thesis: verum