let X be RealNormSpace; :: thesis: for x being Element of REAL
for v being Point of RNS_Real st x = v holds
- x = - v
let x be Element of REAL ; :: thesis: for v being Point of RNS_Real st x = v holds
- x = - v
let v be Point of RNS_Real; :: thesis: ( x = v implies - x = - v )
assume x = v ; :: thesis: - x = - v
then (- 1) * x = (- 1) * v by BINOP_2:def 11;
hence - x = - v by RLVECT_1:16; :: thesis: verum