let p be Point of (TOP-REAL 2); :: thesis: for x being real number
for a, r being real positive number st a <= 1 & |.(p - |[x,(r * a)]|).| = r * a & p `2 <> 0 holds
(+ x,r) . p = a
A1: p = |[(p `1 ),(p `2 )]| by EUCLID:57;
set p1 = p `1 ;
set p2 = p `2 ;
let x be real number ; :: thesis: for a, r being real positive number st a <= 1 & |.(p - |[x,(r * a)]|).| = r * a & p `2 <> 0 holds
(+ x,r) . p = a
let a, r be real positive number ; :: thesis: ( a <= 1 & |.(p - |[x,(r * a)]|).| = r * a & p `2 <> 0 implies (+ x,r) . p = a )
assume A2: a <= 1 ; :: thesis: ( not |.(p - |[x,(r * a)]|).| = r * a or not p `2 <> 0 or (+ x,r) . p = a )
assume A3: ( |.(p - |[x,(r * a)]|).| = r * a & p `2 <> 0 ) ; :: thesis: (+ x,r) . p = a
then ( |.|[((p `1 ) - x),((p `2 ) - (r * a))]|.| ^2 = (r * a) ^2 & |[((p `1 ) - x),((p `2 ) - (r * a))]| `1 = (p `1 ) - x & |[((p `1 ) - x),((p `2 ) - (r * a))]| `2 = (p `2 ) - (r * a) ) by A1, EUCLID:56, EUCLID:66;
then A4: (((p `1 ) - x) ^2 ) + (((p `2 ) - (r * a)) ^2 ) = (r * a) ^2 by JGRAPH_1:46;
then A5: (((p `1 ) - x) ^2 ) + ((p `2 ) ^2 ) = ((2 * (p `2 )) * r) * a ;
( (p `2 ) ^2 > 0 & ((p `1 ) - x) ^2 >= 0 ) by A3, XREAL_1:65;
then (p `2 ) * ((2 * r) * a) > 0 + 0 by A5;
then p `2 > 0 / ((2 * r) * a) ;
then reconsider p2 = p `2 as real positive number ;
A6: ( |[((p `1 ) - x),(p2 - 0 )]| `1 = (p `1 ) - x & |[((p `1 ) - x),p2]| `2 = p2 ) by EUCLID:56;

per cases ( a < 1 or a = 1 ) by A2, XXREAL_0:1;

suppose a < 1 ; :: thesis: (+ x,r) . p = a

then r * a < r by XREAL_1:159;
then reconsider s = r - (r * a) as real positive number by XREAL_1:52;
|.(p - |[x,r]|).| ^2 = |.|[((p `1 ) - x),(p2 - r)]|.| ^2 by A1, EUCLID:66
.= (((p `1 ) - x) ^2 ) + ((p2 - r) ^2 ) by Th13
.= ((((p `1 ) - x) ^2 ) + ((p2 - (a * r)) ^2 )) + (((r - (a * r)) ^2 ) + ((2 * (r - (a * r))) * ((a * r) - p2)))
.= (|.|[((p `1 ) - x),(p2 - (a * r))]|.| ^2 ) + (((r - (a * r)) ^2 ) + ((2 * (r - (a * r))) * ((a * r) - p2))) by Th13
.= ((a * r) ^2 ) + (((((r * r) - (r * p2)) + ((r * a) * r)) - (r * p2)) - (((((a * r) * r) - ((a * r) * p2)) + ((a * r) ^2 )) - ((a * r) * p2))) by A1, A3, EUCLID:66
.= (r ^2 ) - (((1 + 1) * p2) * s) ;
then |.(p - |[x,r]|).| ^2 < r ^2 by XREAL_1:46;
then |.(p - |[x,r]|).| < r by SQUARE_1:77;
then p in Ball |[x,r]|,r by TOPREAL9:7;
then (+ x,r) . p = (|.(|[x,0 ]| - p).| ^2 ) / ((2 * r) * p2) by A1, Def5
.= (|.(p - |[x,0 ]|).| ^2 ) / ((2 * r) * p2) by TOPRNS_1:28
.= (|.|[((p `1 ) - x),(p2 - 0 )]|.| ^2 ) / ((2 * r) * p2) by A1, EUCLID:66
.= ((((p `1 ) - x) ^2 ) + (p2 ^2 )) / ((2 * r) * p2) by A6, JGRAPH_1:46 ;
then ( (+ x,r) . p = (((2 * p2) * r) * a) / ((2 * r) * p2) & a * (((2 * p2) * r) / ((2 * r) * p2)) = a * 1 ) by A4, XCMPLX_1:60;
hence (+ x,r) . p = a by XCMPLX_1:75; :: thesis: verum

end;

suppose A7: a = 1 ; :: thesis: (+ x,r) . p = a

then ( not p in Ball |[x,r]|,r & not p2 is negative ) by A3, TOPREAL9:7;
hence (+ x,r) . p = a by A1, A7, Def5; :: thesis: verum

end;

end;