let X be ComplexUnitarySpace; :: thesis: for x being Point of X holds (0. X) .|. x = 0
let x be Point of X; :: thesis: (0. X) .|. x = 0
H₁(X) .|. x = (x + (- x)) .|. x by RLVECT_1:5
.= (x .|. x) + ((- x) .|. x) by Def11
.= (x .|. x) + (- (x .|. x)) by Th18 ;
hence (0. X) .|. x = 0 ; :: thesis: verum