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