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) by Th52;
A2: (- p2) . 2 = - (p2 . 2) by Th52;
(- p2) . 3 = - (p2 . 3) by Th52;
then p1 + (- p2) = |[((p1 . 1) + (- (p2 . 1))),((p1 . 2) + (- (p2 . 2))),((p1 . 3) + (- (p2 . 3)))]| by A1, A2, Lm2;
hence p1 - p2 = |[((p1 . 1) - (p2 . 1)),((p1 . 2) - (p2 . 2)),((p1 . 3) - (p2 . 3))]| ; :: thesis: verum