let p1, p2 be Point of (TOP-REAL 3); :: thesis: p1 + p2 = |[((p1 `1 ) + (p2 `1 )),((p1 `2 ) + (p2 `2 )),((p1 `3 ) + (p2 `3 ))]|
reconsider p1' = p1, p2' = p2 as Element of REAL 3 by EUCLID:25;
X1: p1 + p2 = p1' + p2' by EUCLID:68;
then len (p1' + p2') = 3 by FINSEQ_1:def 18;
then A1: dom (p1' + p2') = Seg 3 by FINSEQ_1:def 3;
then A2: 1 in dom (p1' + p2') by FINSEQ_1:3;
A3: 2 in dom (p1' + p2') by A1, FINSEQ_1:3;
A4: 3 in dom (p1' + p2') by A1, FINSEQ_1:3;
(p1' + p2') . 1 = (p1' . 1) + (p2' . 1) by A2, VALUED_1:def 1;
then A5: (p1 + p2) `1 = (p1 `1 ) + (p2 `1 ) by A2, EUCLID:68, X1;
(p1' + p2') . 2 = (p1' . 2) + (p2' . 2) by A3, VALUED_1:def 1;
then A6: (p1 + p2) `2 = (p1 `2 ) + (p2 `2 ) by EUCLID:68, X1;
(p1' + p2') . 3 = (p1' . 3) + (p2' . 3) by A4, VALUED_1:def 1;
then (p1 + p2) `3 = (p1 `3 ) + (p2 `3 ) by EUCLID:68, X1;
hence p1 + p2 = |[((p1 `1 ) + (p2 `1 )),((p1 `2 ) + (p2 `2 )),((p1 `3 ) + (p2 `3 ))]| by A5, A6, Th3; :: thesis: verum