let V be RealNormSpace; :: thesis: for x being Point of V
for y being Point of (DualSp V) holds (- x) .|. y = - (x .|. y)
let x be Point of V; :: thesis: for y being Point of (DualSp V) holds (- x) .|. y = - (x .|. y)
let y be Point of (DualSp V); :: thesis: (- x) .|. y = - (x .|. y)
thus (- x) .|. y = ((- 1) * x) .|. y by RLVECT_1:16
.= (- 1) * (x .|. y) by Th6
.= - (x .|. y) ; :: thesis: verum