let p1, p2 be Point of (TOP-REAL 2); :: thesis: 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); :: thesis: ( u1 = p1 & u2 = p2 implies (Pitag_dist 2) . u1,u2 = sqrt ((((p1 `1 ) - (p2 `1 )) ^2 ) + (((p1 `2 ) - (p2 `2 )) ^2 )) )
assume A1: ( u1 = p1 & u2 = p2 ) ; :: thesis: (Pitag_dist 2) . u1,u2 = sqrt ((((p1 `1 ) - (p2 `1 )) ^2 ) + (((p1 `2 ) - (p2 `2 )) ^2 ))
A2: p1 = |[(p1 `1 ),(p1 `2 )]| by EUCLID:57;
A3: u2 = <*(p2 `1 ),(p2 `2 )*> by A1, EUCLID:57;
reconsider v1 = u1, v2 = u2 as Element of REAL 2 ;
v1 - v2 = <*(diffreal . (p1 `1 ),(p2 `1 )),(diffreal . (p1 `2 ),(p2 `2 ))*> by A1, A2, A3, 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 A4: 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 A4, RVSUM_1:107; :: thesis: verum