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