let V be RealNormSpace; :: thesis: for x being Point of V
for y, z being Point of (DualSp V) holds x .|. (y - z) = (x .|. y) - (x .|. z)
let x be Point of V; :: thesis: for y, z being Point of (DualSp V) holds x .|. (y - z) = (x .|. y) - (x .|. z)
let y, z be Point of (DualSp V); :: thesis: x .|. (y - z) = (x .|. y) - (x .|. z)
thus x .|. (y - z) = (x .|. y) + (x .|. (- z)) by DUALSP01:29
.= (x .|. y) + (- (x .|. z)) by Th9
.= (x .|. y) - (x .|. z) ; :: thesis: verum