let q be Point of (TOP-REAL 2); :: thesis: for r being Real holds dist (|[0,0]|,(r * q)) = |.r.| * (dist (|[0,0]|,q))
let r be Real; :: thesis: dist (|[0,0]|,(r * q)) = |.r.| * (dist (|[0,0]|,q))
A1: ( r ^2 >= 0 & (q `1) ^2 >= 0 ) by XREAL_1:63;
A2: (q `2) ^2 >= 0 by XREAL_1:63;
A3: ( |[0,0]| `1 = 0 & |[0,0]| `2 = 0 ) by EUCLID:52;
then A4: dist (|[0,0]|,q) = sqrt (((0 - (q `1)) ^2) + ((0 - (q `2)) ^2)) by TOPREAL6:92
.= 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:92
.= sqrt ((((r * q) `1) ^2) + ((- ((r * q) `2)) ^2))
.= sqrt (((r * (q `1)) ^2) + (((r * q) `2) ^2)) by TOPREAL3:4
.= sqrt (((r ^2) * ((q `1) ^2)) + ((r * (q `2)) ^2)) by TOPREAL3:4
.= sqrt ((r ^2) * (((q `1) ^2) + ((q `2) ^2)))
.= (sqrt (r ^2)) * (sqrt (((q `1) ^2) + ((q `2) ^2))) by A1, A2, SQUARE_1:29
.= |.r.| * (dist (|[0,0]|,q)) by A4, COMPLEX1:72 ; :: thesis: verum