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) = x .|. ((- 1) * y) by RLVECT_1:16
.= (- 1) * (x .|. y) by DUALSP01:30
.= - (x .|. y) ; :: thesis: verum