let p1, p2 be Point of (TOP-REAL 2); p1 + p2 = |[((p1 `1 ) + (p2 `1 )),((p1 `2 ) + (p2 `2 ))]|
TopStruct(# the carrier of (TOP-REAL 2),the topology of (TOP-REAL 2) #) = TopSpaceMetr (Euclid 2)
by Def8;
then reconsider p19 = p1, p29 = p2 as Element of REAL 2 ;
len (p19 + p29) = 2
by FINSEQ_1:def 18;
then A1:
dom (p19 + p29) = Seg 2
by FINSEQ_1:def 3;
2 in {1,2}
by TARSKI:def 2;
then A2:
(p1 + p2) `2 = (p1 `2 ) + (p2 `2 )
by A1, FINSEQ_1:4, VALUED_1:def 1;
1 in {1,2}
by TARSKI:def 2;
then
(p1 + p2) `1 = (p1 `1 ) + (p2 `1 )
by A1, FINSEQ_1:4, VALUED_1:def 1;
hence
p1 + p2 = |[((p1 `1 ) + (p2 `1 )),((p1 `2 ) + (p2 `2 ))]|
by A2, Th57; verum