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