let q be Point of (TOP-REAL 2); :: thesis: for r being Real holds dist |[0 ,0 ]|,(r * q) = (abs r) * (dist |[0 ,0 ]|,q)
let r be Real; :: thesis: dist |[0 ,0 ]|,(r * q) = (abs r) * (dist |[0 ,0 ]|,q)
A1: ( r ^2 >= 0 & (q `1 ) ^2 >= 0 ) by XREAL_1:65;
A2: (q `2 ) ^2 >= 0 by XREAL_1:65;
A3: ( |[0 ,0 ]| `1 = 0 & |[0 ,0 ]| `2 = 0 ) by EUCLID:56;
then A4: dist |[0 ,0 ]|,q = sqrt (((0 - (q `1 )) ^2 ) + ((0 - (q `2 )) ^2 )) by TOPREAL6:101
.= sqrt (((q `1 ) ^2 ) + ((q `2 ) ^2 )) ;
thus dist |[0 ,0 ]|,(r * q) = sqrt (((0 - ((r * q) `1 )) ^2 ) + ((0 - ((r * q) `2 )) ^2 )) by A3, TOPREAL6:101
.= sqrt ((((r * q) `1 ) ^2 ) + ((- ((r * q) `2 )) ^2 ))
.= sqrt (((r * (q `1 )) ^2 ) + (((r * q) `2 ) ^2 )) by TOPREAL3:9
.= sqrt (((r ^2 ) * ((q `1 ) ^2 )) + ((r * (q `2 )) ^2 )) by TOPREAL3:9
.= sqrt ((r ^2 ) * (((q `1 ) ^2 ) + ((q `2 ) ^2 )))
.= (sqrt (r ^2 )) * (sqrt (((q `1 ) ^2 ) + ((q `2 ) ^2 ))) by A1, A2, SQUARE_1:97
.= (abs r) * (dist |[0 ,0 ]|,q) by A4, COMPLEX1:158 ; :: thesis: verum