let p be Element of REAL 3; :: thesis: - p = |[(- (p . 1)),(- (p . 2)),(- (p . 3))]|
- p = |[((- 1) * (p . 1)),((- 1) * (p . 2)),((- 1) * (p . 3))]| by Lm1
.= |[(- (p . 1)),(- (p . 2)),(- (p . 3))]| ;
hence - p = |[(- (p . 1)),(- (p . 2)),(- (p . 3))]| ; :: thesis: verum