let p be Point of (TOP-REAL 2); :: thesis: for x being Real
for a, r being positive Real 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; :: thesis: for a, r being positive Real st a <= 1 & |.(p - |[x,(r * a)]|).| = r * a & p `2 <> 0 holds
(+ (x,r)) . p = a
let a, r be positive Real; :: 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:52;
A3: |[((p `1) - x),((p `2) - (r * a))]| `2 = (p `2) - (r * a) by EUCLID:52;
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:53;
then |.|[((p `1) - x),((p `2) - (r * a))]|.| ^2 = (r * a) ^2 by A4, EUCLID:62;
then A7: (((p `1) - x) ^2) + (((p `2) - (r * a)) ^2) = (r * a) ^2 by A2, A3, JGRAPH_1:29;
then A8: (((p `1) - x) ^2) + ((p `2) ^2) = ((2 * (p `2)) * r) * a ;
((p `1) - x) ^2 >= 0 by XREAL_1:63;
then reconsider p2 = p `2 as positive Real by A5, A8;
A9: |[((p `1) - x),(p2 - 0)]| `1 = (p `1) - x by EUCLID:52;
A10: |[((p `1) - x),p2]| `2 = p2 by EUCLID:52;

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:157;
then reconsider s = r - (r * a) as positive Real by XREAL_1:50;
|.(p - |[x,r]|).| ^2 = |.|[((p `1) - x),(p2 - r)]|.| ^2 by A6, EUCLID:62
.= (((p `1) - x) ^2) + ((p2 - r) ^2) by Th9
.= ((((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 Th9
.= ((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:62
.= (r ^2) - (((1 + 1) * p2) * s) ;
then |.(p - |[x,r]|).| ^2 < r ^2 by XREAL_1:44;
then |.(p - |[x,r]|).| < r by SQUARE_1:15;
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:27
.= (|.|[((p `1) - x),(p2 - 0)]|.| ^2) / ((2 * r) * p2) by A6, EUCLID:62
.= ((((p `1) - x) ^2) + (p2 ^2)) / ((2 * r) * p2) by A9, A10, JGRAPH_1:29 ;
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:74; :: 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;