let p1, p2 be Element of REAL 3; :: thesis: p1 - p2 = |[((p1 . 1) - (p2 . 1)),((p1 . 2) - (p2 . 2)),((p1 . 3) - (p2 . 3))]|
A2: (- p2) . 1 = - (p2 . 1) by Th11;
A3: (- p2) . 2 = - (p2 . 2) by Th11;
A4: (- p2) . 3 = - (p2 . 3) by Th11;
p1 + (- p2) = |[((p1 . 1) + (- (p2 . 1))),((p1 . 2) + (- (p2 . 2))),((p1 . 3) + (- (p2 . 3)))]| by A2, A3, A4, Lm4;
hence p1 - p2 = |[((p1 . 1) - (p2 . 1)),((p1 . 2) - (p2 . 2)),((p1 . 3) - (p2 . 3))]| ; :: thesis: verum