let r1, s1, r2, s2 be real number ; :: thesis: for u, v being Point of (Euclid 2) st u = |[r1,s1]| & v = |[r2,s2]| holds
dist u,v = sqrt (((r1 - r2) ^2 ) + ((s1 - s2) ^2 ))
let u, v be Point of (Euclid 2); :: thesis: ( u = |[r1,s1]| & v = |[r2,s2]| implies dist u,v = sqrt (((r1 - r2) ^2 ) + ((s1 - s2) ^2 )) )
assume that
A1: u = |[r1,s1]| and
A2: v = |[r2,s2]| ; :: thesis: dist u,v = sqrt (((r1 - r2) ^2 ) + ((s1 - s2) ^2 ))
A3: |[r1,s1]| `1 = r1 by EUCLID:56;
A4: |[r2,s2]| `2 = s2 by EUCLID:56;
A5: |[r2,s2]| `1 = r2 by EUCLID:56;
A6: |[r1,s1]| `2 = s1 by EUCLID:56;
thus dist u,v = (Pitag_dist 2) . u,v by METRIC_1:def 1
.= sqrt (((r1 - r2) ^2 ) + ((s1 - s2) ^2 )) by A1, A2, A3, A6, A5, A4, TOPREAL3:12 ; :: thesis: verum