let x, y be Real; :: thesis: for r being positive Real st x <> y holds
(+ (x,r)) . |[y,0]| = 1
let r be positive Real; :: thesis: ( x <> y implies (+ (x,r)) . |[y,0]| = 1 )
A1: ( |.(x - y).| = x - y or |.(x - y).| = - (x - y) ) by ABSVALUE:1;
A2: |[(x - y),r]| `2 = r by EUCLID:52;
|[(x - y),r]| `1 = x - y by EUCLID:52;
then A3: |.|[(x - y),r]|.| ^2 = (r ^2) + ((x - y) ^2) by A2, JGRAPH_1:29;
assume A4: x <> y ; :: thesis: (+ (x,r)) . |[y,0]| = 1
then x - y <> 0 ;
then A5: |.(x - y).| > 0 by COMPLEX1:47;
then |.(x - y).| ^2 <> 0 ;
then |.|[(x - y),r]|.| ^2 > r ^2 by A1, A5, A3, XREAL_1:29;
then |.|[(x - y),(r - 0)]|.| > r by SQUARE_1:15;
then |.(|[x,r]| - |[y,0]|).| > r by EUCLID:62;
then |.(|[y,0]| - |[x,r]|).| > r by TOPRNS_1:27;
then not |[y,0]| in Ball (|[x,r]|,r) by TOPREAL9:7;
hence (+ (x,r)) . |[y,0]| = 1 by A4, Def5; :: thesis: verum