let p be Element of REAL 3; :: thesis: - p = |[(- (p . 1)),(- (p . 2)),(- (p . 3))]|
reconsider r = - 1 as Element of REAL by XREAL_0:def 1;
r * p = |[((- 1) * (p . 1)),((- 1) * (p . 2)),((- 1) * (p . 3))]| by Th49
.= |[(- (p . 1)),(- (p . 2)),(- (p . 3))]| ;
hence - p = |[(- (p . 1)),(- (p . 2)),(- (p . 3))]| ; :: thesis: verum