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