let X be RealUnitarySpace; :: 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 Def2
.= (x .|. x) + (- (x .|. x)) by Th13 ;
hence (0. X) .|. x = 0 ; :: thesis: verum