let V be RealNormSpace; :: thesis: for x being Point of (DualSp V) holds (0. V) .|. x = 0
let x be Point of (DualSp V); :: thesis: (0. V) .|. x = 0
thus (0. V) .|. x = (0 * (0. V)) .|. x
.= 0 * ((0. V) .|. x) by Th6
.= 0 ; :: thesis: verum