let RNS be RealNormSpace; :: thesis: for x being Point of RNS holds ||.(- x).|| = ||.x.||
let x be Point of RNS; :: thesis: ||.(- x).|| = ||.x.||
A1: |.(- 1).| = - (- 1) by ABSVALUE:def 1
.= 1 ;
||.(- x).|| = ||.((- 1) * x).|| by RLVECT_1:16
.= |.(- 1).| * ||.x.|| by Def1 ;
hence ||.(- x).|| = ||.x.|| by A1; :: thesis: verum