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 Def11
.= 0c by Th24, COMPLEX1:28 ;
hence x .|. (0. X) = 0 ; :: thesis: verum