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 ;
( p1 = |[(p1 `1 ),(p1 `2 )]| & u2 = <*(p2 `1 ),(p2 `2 )*> )
by A2, EUCLID:57;
then v1 - v2 =
<*(diffreal . (p1 `1 ),(p2 `1 )),(diffreal . (p1 `2 ),(p2 `2 ))*>
by A1, FINSEQ_2:89
.=
<*((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:40
.=
<*(abs ((p1 `1 ) - (p2 `1 ))),(absreal . ((p1 `2 ) - (p2 `2 )))*>
by EUCLID:def 2
.=
<*(abs ((p1 `1 ) - (p2 `1 ))),(abs ((p1 `2 ) - (p2 `2 )))*>
by EUCLID:def 2
;
then A3: sqr (abs (v1 - v2)) =
<*(sqrreal . (abs ((p1 `1 ) - (p2 `1 )))),(sqrreal . (abs ((p1 `2 ) - (p2 `2 ))))*>
by FINSEQ_2:40
.=
<*((abs ((p1 `1 ) - (p2 `1 ))) ^2 ),(sqrreal . (abs ((p1 `2 ) - (p2 `2 ))))*>
by RVSUM_1:def 2
.=
<*((abs ((p1 `1 ) - (p2 `1 ))) ^2 ),((abs ((p1 `2 ) - (p2 `2 ))) ^2 )*>
by RVSUM_1:def 2
.=
<*(((p1 `1 ) - (p2 `1 )) ^2 ),((abs ((p1 `2 ) - (p2 `2 ))) ^2 )*>
by COMPLEX1:161
.=
<*(((p1 `1 ) - (p2 `1 )) ^2 ),(((p1 `2 ) - (p2 `2 )) ^2 )*>
by COMPLEX1:161
;
(Pitag_dist 2) . u1,u2 =
|.(v1 - v2).|
by EUCLID:def 6
.=
sqrt (Sum (sqr (abs (v1 - v2))))
by EUCLID:29
;
hence
(Pitag_dist 2) . u1,u2 = sqrt ((((p1 `1 ) - (p2 `1 )) ^2 ) + (((p1 `2 ) - (p2 `2 )) ^2 ))
by A3, RVSUM_1:107; verum