let X be ComplexUnitarySpace; :: thesis: for x being Point of X holds ||.(- x).|| = ||.x.||
let x be Point of X; :: thesis: ||.(- x).|| = ||.x.||
||.(- x).|| = ||.((- 1r) * x).|| by CLVECT_1:3
.= |.(- 1r).| * ||.x.|| by Th38
.= |.1r.| * ||.x.|| by COMPLEX1:52 ;
hence ||.(- x).|| = ||.x.|| by COMPLEX1:48; :: thesis: verum