let x, y be real number ; :: thesis: for r being real positive number st x <> y holds
(+ x,r) . |[y,0 ]| = 1
let r be real positive number ; :: thesis: ( x <> y implies (+ x,r) . |[y,0 ]| = 1 )
assume A1: x <> y ; :: thesis: (+ x,r) . |[y,0 ]| = 1
then x - y <> 0 ;
then |.(x - y).| > 0 by COMPLEX1:133;
then ( ( |.(x - y).| = x - y or |.(x - y).| = - (x - y) ) & |.(x - y).| ^2 <> 0 & |.(x - y).| ^2 >= 0 & |[(x - y),r]| `1 = x - y & |[(x - y),r]| `2 = r ) by ABSVALUE:1, EUCLID:56;
then ( (x - y) ^2 > 0 & |.|[(x - y),r]|.| ^2 = (r ^2 ) + ((x - y) ^2 ) ) by JGRAPH_1:46;
then ( |.|[(x - y),r]|.| ^2 > r ^2 & |.|[(x - y),r]|.| >= 0 ) by XREAL_1:31;
then |.|[(x - y),(r - 0 )]|.| > r by SQUARE_1:77;
then |.(|[x,r]| - |[y,0 ]|).| > r by EUCLID:66;
then |.(|[y,0 ]| - |[x,r]|).| > r by TOPRNS_1:28;
then not |[y,0 ]| in Ball |[x,r]|,r by TOPREAL9:7;
hence (+ x,r) . |[y,0 ]| = 1 by A1, Def5; :: thesis: verum