let p1, p2 be Point of (TOP-REAL 3); p1 + p2 = |[((p1 `1) + (p2 `1)),((p1 `2) + (p2 `2)),((p1 `3) + (p2 `3))]|
reconsider p19 = p1, p29 = p2 as Element of REAL 3 by EUCLID:22;
len (p19 + p29) = 3
by CARD_1:def 7;
then A1:
dom (p19 + p29) = Seg 3
by FINSEQ_1:def 3;
then
2 in dom (p19 + p29)
by FINSEQ_1:1;
then
(p19 + p29) . 2 = (p19 . 2) + (p29 . 2)
by VALUED_1:def 1;
then A2:
(p1 + p2) `2 = (p1 `2) + (p2 `2)
by EUCLID:64;
3 in dom (p19 + p29)
by A1, FINSEQ_1:1;
then
(p19 + p29) . 3 = (p19 . 3) + (p29 . 3)
by VALUED_1:def 1;
then A3:
(p1 + p2) `3 = (p1 `3) + (p2 `3)
by EUCLID:64;
1 in dom (p19 + p29)
by A1, FINSEQ_1:1;
then
(p19 + p29) . 1 = (p19 . 1) + (p29 . 1)
by VALUED_1:def 1;
then
(p1 + p2) `1 = (p1 `1) + (p2 `1)
by EUCLID:64;
hence
p1 + p2 = |[((p1 `1) + (p2 `1)),((p1 `2) + (p2 `2)),((p1 `3) + (p2 `3))]|
by A2, A3, Th3; verum