let p be Point of (TOP-REAL 3); :: thesis: - p = |[(- (p `1)),(- (p `2)),(- (p `3))]|
thus - p = (- 1) * p by RLVECT_1:16
.= |[((- 1) * (p `1)),((- 1) * (p `2)),((- 1) * (p `3))]| by Th7
.= |[(- (p `1)),(- (p `2)),(- (p `3))]| ; :: thesis: verum