let p1, p2 be Element of REAL 3; 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, FINSEQ_1:45
.=
|[((p1 . 1) + (- (p2 . 1))),((p1 . 2) + (- (p2 . 2))),((p1 . 3) + ((- p2) . 3))]|
by A1, FINSEQ_1:45
.=
|[((p1 . 1) + (- (p2 . 1))),((p1 . 2) + (- (p2 . 2))),((p1 . 3) + (- (p2 . 3)))]|
by A1, FINSEQ_1:45
;
hence
p1 + (- p2) = |[((p1 . 1) - (p2 . 1)),((p1 . 2) - (p2 . 2)),((p1 . 3) - (p2 . 3))]|
; verum