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:134, COMPLEX1:138;
||.(- x).|| = ||.((- 1r ) * x).|| by Th4
.= |.(- 1r ).| * ||.x.|| by Def14 ;
hence ||.(- x).|| = ||.x.|| by A1; :: thesis: verum