let p1, p2 be Point of (TOP-REAL 2); for u1, u2 being Point of (Euclid 2) st u1 = p1 & u2 = p2 holds
(Pitag_dist 2) . (u1,u2) = sqrt ((((p1 `1) - (p2 `1)) ^2) + (((p1 `2) - (p2 `2)) ^2))
let u1, u2 be Point of (Euclid 2); ( u1 = p1 & u2 = p2 implies (Pitag_dist 2) . (u1,u2) = sqrt ((((p1 `1) - (p2 `1)) ^2) + (((p1 `2) - (p2 `2)) ^2)) )
assume that
A1:
u1 = p1
and
A2:
u2 = p2
; (Pitag_dist 2) . (u1,u2) = sqrt ((((p1 `1) - (p2 `1)) ^2) + (((p1 `2) - (p2 `2)) ^2))
reconsider v1 = u1, v2 = u2 as Element of REAL 2 ;
reconsider p11 = p1 `1 , p21 = p2 `1 , p12 = p1 `2 , p22 = p2 `2 as Element of REAL by XREAL_0:def 1;
( p1 = |[(p1 `1),(p1 `2)]| & u2 = <*(p2 `1),(p2 `2)*> )
by A2, EUCLID:53;
then v1 - v2 =
<*(diffreal . (p11,p21)),(diffreal . (p12,p22))*>
by A1, FINSEQ_2:75
.=
<*((p1 `1) - (p2 `1)),(diffreal . ((p1 `2),(p2 `2)))*>
by BINOP_2:def 10
.=
<*((p1 `1) - (p2 `1)),((p1 `2) - (p2 `2))*>
by BINOP_2:def 10
;
then abs (v1 - v2) =
<*(absreal . ((p1 `1) - (p2 `1))),(absreal . ((p1 `2) - (p2 `2)))*>
by FINSEQ_2:36
.=
<*|.((p1 `1) - (p2 `1)).|,(absreal . ((p1 `2) - (p2 `2)))*>
by EUCLID:def 2
.=
<*|.((p1 `1) - (p2 `1)).|,|.((p1 `2) - (p2 `2)).|*>
by EUCLID:def 2
;
then A3: sqr (abs (v1 - v2)) =
<*(sqrreal . |.((p1 `1) - (p2 `1)).|),(sqrreal . |.((p1 `2) - (p2 `2)).|)*>
by FINSEQ_2:36
.=
<*(|.((p1 `1) - (p2 `1)).| ^2),(sqrreal . |.((p1 `2) - (p2 `2)).|)*>
by RVSUM_1:def 2
.=
<*(|.((p1 `1) - (p2 `1)).| ^2),(|.((p1 `2) - (p2 `2)).| ^2)*>
by RVSUM_1:def 2
.=
<*(((p1 `1) - (p2 `1)) ^2),(|.((p1 `2) - (p2 `2)).| ^2)*>
by COMPLEX1:75
.=
<*(((p1 `1) - (p2 `1)) ^2),(((p1 `2) - (p2 `2)) ^2)*>
by COMPLEX1:75
;
(Pitag_dist 2) . (u1,u2) =
|.(v1 - v2).|
by EUCLID:def 6
.=
sqrt (Sum (sqr (abs (v1 - v2))))
by EUCLID:25
;
hence
(Pitag_dist 2) . (u1,u2) = sqrt ((((p1 `1) - (p2 `1)) ^2) + (((p1 `2) - (p2 `2)) ^2))
by A3, RVSUM_1:77; verum