let CNS be ComplexNormSpace; :: thesis: for x being Point of CNS holds ||.(- x).|| = ||.x.||
let x be Point of CNS; :: thesis: ||.(- x).|| = ||.x.||
A1: |.(- 1r).| = 1 by COMPLEX1:48, COMPLEX1:52;
||.(- x).|| = ||.((- 1r) * x).|| by Th3
.= |.(- 1r).| * ||.x.|| by Def13 ;
hence ||.(- x).|| = ||.x.|| by A1; :: thesis: verum