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