A1: LC p <> 0. L ;
LC (((1. L) / (LC p)) * p) = ((1. L) / (LC p)) * (LC p) by Th18
.= (1. L) * (((LC p) ") * (LC p))
.= (1. L) * (1. L) by A1, VECTSP_1:def 10
.= 1. L ;
hence ((1. L) / (LC p)) * p is normalized ; :: thesis: verum