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