let q1, q, q2 be Point of (TOP-REAL 2); dist (q1 + q),(q2 + q) = dist q1,q2
A1: ((q1 + q) `1 ) - ((q2 + q) `1 ) =
((q1 `1 ) + (q `1 )) - ((q2 + q) `1 )
by TOPREAL3:7
.=
((q1 `1 ) + (q `1 )) - ((q2 `1 ) + (q `1 ))
by TOPREAL3:7
.=
((q1 `1 ) - (q2 `1 )) + 0
;
A2: ((q1 + q) `2 ) - ((q2 + q) `2 ) =
((q1 `2 ) + (q `2 )) - ((q2 + q) `2 )
by TOPREAL3:7
.=
((q1 `2 ) + (q `2 )) - ((q2 `2 ) + (q `2 ))
by TOPREAL3:7
.=
((q1 `2 ) - (q2 `2 )) + 0
;
thus dist (q1 + q),(q2 + q) =
sqrt (((((q1 + q) `1 ) - ((q2 + q) `1 )) ^2 ) + ((((q1 + q) `2 ) - ((q2 + q) `2 )) ^2 ))
by TOPREAL6:101
.=
dist q1,q2
by A1, A2, TOPREAL6:101
; verum