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
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 A1: a <= 1 ; :: thesis: ( not |.(p - |[x,(r * a)]|).| = r * a or not p `2 <> 0 or (+ x,r) . p = a )
A2: |[((p `1 ) - x),((p `2 ) - (r * a))]| `1 = (p `1 ) - x by EUCLID:56;
A3: |[((p `1 ) - x),((p `2 ) - (r * a))]| `2 = (p `2 ) - (r * a) by EUCLID:56;
assume that
A4: |.(p - |[x,(r * a)]|).| = r * a and
A5: p `2 <> 0 ; :: thesis: (+ x,r) . p = a
A6: p = |[(p `1 ),(p `2 )]| by EUCLID:57;
then |.|[((p `1 ) - x),((p `2 ) - (r * a))]|.| ^2 = (r * a) ^2 by A4, EUCLID:66;
then A7: (((p `1 ) - x) ^2 ) + (((p `2 ) - (r * a)) ^2 ) = (r * a) ^2 by A2, A3, JGRAPH_1:46;
then A8: (((p `1 ) - x) ^2 ) + ((p `2 ) ^2 ) = ((2 * (p `2 )) * r) * a ;
((p `1 ) - x) ^2 >= 0 by XREAL_1:65;
then reconsider p2 = p `2 as real positive number by A5, A8;
A9: |[((p `1 ) - x),(p2 - 0 )]| `1 = (p `1 ) - x by EUCLID:56;
A10: |[((p `1 ) - x),p2]| `2 = p2 by EUCLID:56;

per cases ( a < 1 or a = 1 ) by A1, 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 A6, 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 A6, A4, 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 A6, Def5
.= (|.(p - |[x,0 ]|).| ^2 ) / ((2 * r) * p2) by TOPRNS_1:28
.= (|.|[((p `1 ) - x),(p2 - 0 )]|.| ^2 ) / ((2 * r) * p2) by A6, EUCLID:66
.= ((((p `1 ) - x) ^2 ) + (p2 ^2 )) / ((2 * r) * p2) by A9, A10, JGRAPH_1:46 ;
then A11: (+ x,r) . p = (((2 * p2) * r) * a) / ((2 * r) * p2) by A7;
a * (((2 * p2) * r) / ((2 * r) * p2)) = a * 1 by XCMPLX_1:60;
hence (+ x,r) . p = a by A11, XCMPLX_1:75; :: thesis: verum

end;

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

A13: not p2 is negative ;
not p in Ball |[x,r]|,r by A12, A4, TOPREAL9:7;
hence (+ x,r) . p = a by A13, A6, A12, Def5; :: thesis: verum

end;

end;