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:59;
(- (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:12;
Re (((- p) `1) + (((- p) `2) * <i>)) = (- p) `1 by COMPLEX1:12;
then ( Im (((- p) `1) + (((- p) `2) * <i>)) = (- p) `2 & Re (((- p) `1) + (((- p) `2) * <i>)) = - (p `1) ) by A1, COMPLEX1:12, EUCLID:52;
hence ((- p) `1) + (((- p) `2) * <i>) = (- (p `1)) + ((- (p `2)) * <i>) by A1, A2, EUCLID:52; :: thesis: verum