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