let X be RealNormSpace; :: thesis: for x being Point of (DualSp X)
for v being Point of (R_NormSpace_of_BoundedLinearOperators (X,RNS_Real)) st x = v holds
- x = - v
let x be Point of (DualSp X); :: thesis: for v being Point of (R_NormSpace_of_BoundedLinearOperators (X,RNS_Real)) st x = v holds
- x = - v
let v be Point of (R_NormSpace_of_BoundedLinearOperators (X,RNS_Real)); :: thesis: ( x = v implies - x = - v )
assume AS: x = v ; :: thesis: - x = - v
A1: - 1 is Element of REAL by XREAL_0:def 1;
thus - x = (- 1) * x by RLVECT_1:16
.= (- 1) * v by AS, A1, LMN9
.= - v by RLVECT_1:16 ; :: thesis: verum