let p be Point of ; :: thesis: euc2cpx (- p) = - (euc2cpx p)
- (euc2cpx p) = (- (p `1 )) + ((- (p `2 )) * <i> ) ;
hence euc2cpx (- p) = - (euc2cpx p) by Th16; :: thesis: verum