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