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