let X be ComplexUnitarySpace; :: thesis: for x being Point of X holds x .|. (0. X) = 0
let x be Point of X; :: thesis: x .|. (0. X) = 0
x .|. (0. X) = ((0. X) .|. x) *' by Def13
.= 0c by Th31, COMPLEX1:113 ;
hence x .|. (0. X) = 0 ; :: thesis: verum