let p be Point of (TOP-REAL 2); :: thesis: ((- p) `1 ) + (((- p) `2 ) * <i> ) = (- (p `1 )) + ((- (p `2 )) * <i> )
A1: - p = |[(- (p `1 )),(- (p `2 ))]| by EUCLID:63;
(- (p `1 )) + ((- (p `2 )) * <i> ) = (- (p `1 )) + ((- (p `2 )) * <i> ) ;
then A2: ( Re ((- (p `1 )) + (- ((p `2 ) * <i> ))) = - (p `1 ) & Im ((- (p `1 )) + (- ((p `2 ) * <i> ))) = - (p `2 ) ) by COMPLEX1:28;
Re (((- p) `1 ) + (((- p) `2 ) * <i> )) = (- p) `1 by COMPLEX1:28;
then ( Im (((- p) `1 ) + (((- p) `2 ) * <i> )) = (- p) `2 & Re (((- p) `1 ) + (((- p) `2 ) * <i> )) = - (p `1 ) ) by A1, COMPLEX1:28, EUCLID:56;
hence ((- p) `1 ) + (((- p) `2 ) * <i> ) = (- (p `1 )) + ((- (p `2 )) * <i> ) by A1, A2, COMPLEX1:9, EUCLID:56; :: thesis: verum