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