let q, q1, 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:2
.=
((q1 `1) + (q `1)) - ((q2 `1) + (q `1))
by TOPREAL3:2
.=
((q1 `1) - (q2 `1)) + 0
;
A2: ((q1 + q) `2) - ((q2 + q) `2) =
((q1 `2) + (q `2)) - ((q2 + q) `2)
by TOPREAL3:2
.=
((q1 `2) + (q `2)) - ((q2 `2) + (q `2))
by TOPREAL3:2
.=
((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:92
.=
dist (q1,q2)
by A1, A2, TOPREAL6:92
; verum