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