let p be Point of (TOP-REAL 2); :: thesis: for e being Point of (Euclid 2)
for r being Real st p = e holds
product ((1,2) --> (].((p `1) - (r / (sqrt 2))),((p `1) + (r / (sqrt 2))).[,].((p `2) - (r / (sqrt 2))),((p `2) + (r / (sqrt 2))).[)) c= Ball (e,r)
let e be Point of (Euclid 2); :: thesis: for r being Real st p = e holds
product ((1,2) --> (].((p `1) - (r / (sqrt 2))),((p `1) + (r / (sqrt 2))).[,].((p `2) - (r / (sqrt 2))),((p `2) + (r / (sqrt 2))).[)) c= Ball (e,r)
let r be Real; :: thesis: ( p = e implies product ((1,2) --> (].((p `1) - (r / (sqrt 2))),((p `1) + (r / (sqrt 2))).[,].((p `2) - (r / (sqrt 2))),((p `2) + (r / (sqrt 2))).[)) c= Ball (e,r) )
set A = ].((p `1) - (r / (sqrt 2))),((p `1) + (r / (sqrt 2))).[;
set B = ].((p `2) - (r / (sqrt 2))),((p `2) + (r / (sqrt 2))).[;
set f = (1,2) --> (].((p `1) - (r / (sqrt 2))),((p `1) + (r / (sqrt 2))).[,].((p `2) - (r / (sqrt 2))),((p `2) + (r / (sqrt 2))).[);
assume A1: p = e ; :: thesis: product ((1,2) --> (].((p `1) - (r / (sqrt 2))),((p `1) + (r / (sqrt 2))).[,].((p `2) - (r / (sqrt 2))),((p `2) + (r / (sqrt 2))).[)) c= Ball (e,r)
let a be object ; :: according to TARSKI:def 3 :: thesis: ( not a in product ((1,2) --> (].((p `1) - (r / (sqrt 2))),((p `1) + (r / (sqrt 2))).[,].((p `2) - (r / (sqrt 2))),((p `2) + (r / (sqrt 2))).[)) or a in Ball (e,r) )
A2: ].((p `1) - (r / (sqrt 2))),((p `1) + (r / (sqrt 2))).[ = { m where m is Real : ( (p `1) - (r / (sqrt 2)) < m & m < (p `1) + (r / (sqrt 2)) ) } by RCOMP_1:def 2;
A3: ((1,2) --> (].((p `1) - (r / (sqrt 2))),((p `1) + (r / (sqrt 2))).[,].((p `2) - (r / (sqrt 2))),((p `2) + (r / (sqrt 2))).[)) . 2 = ].((p `2) - (r / (sqrt 2))),((p `2) + (r / (sqrt 2))).[ by FUNCT_4:63;
A4: ].((p `2) - (r / (sqrt 2))),((p `2) + (r / (sqrt 2))).[ = { n where n is Real : ( (p `2) - (r / (sqrt 2)) < n & n < (p `2) + (r / (sqrt 2)) ) } by RCOMP_1:def 2;
A5: ((1,2) --> (].((p `1) - (r / (sqrt 2))),((p `1) + (r / (sqrt 2))).[,].((p `2) - (r / (sqrt 2))),((p `2) + (r / (sqrt 2))).[)) . 1 = ].((p `1) - (r / (sqrt 2))),((p `1) + (r / (sqrt 2))).[ by FUNCT_4:63;
assume a in product ((1,2) --> (].((p `1) - (r / (sqrt 2))),((p `1) + (r / (sqrt 2))).[,].((p `2) - (r / (sqrt 2))),((p `2) + (r / (sqrt 2))).[)) ; :: thesis: a in Ball (e,r)
then consider g being Function such that
A6: a = g and
A7: dom g = dom ((1,2) --> (].((p `1) - (r / (sqrt 2))),((p `1) + (r / (sqrt 2))).[,].((p `2) - (r / (sqrt 2))),((p `2) + (r / (sqrt 2))).[)) and
A8: for x being object st x in dom ((1,2) --> (].((p `1) - (r / (sqrt 2))),((p `1) + (r / (sqrt 2))).[,].((p `2) - (r / (sqrt 2))),((p `2) + (r / (sqrt 2))).[)) holds
g . x in ((1,2) --> (].((p `1) - (r / (sqrt 2))),((p `1) + (r / (sqrt 2))).[,].((p `2) - (r / (sqrt 2))),((p `2) + (r / (sqrt 2))).[)) . x by CARD_3:def 5;
A9: dom ((1,2) --> (].((p `1) - (r / (sqrt 2))),((p `1) + (r / (sqrt 2))).[,].((p `2) - (r / (sqrt 2))),((p `2) + (r / (sqrt 2))).[)) = {1,2} by FUNCT_4:62;
then 1 in dom ((1,2) --> (].((p `1) - (r / (sqrt 2))),((p `1) + (r / (sqrt 2))).[,].((p `2) - (r / (sqrt 2))),((p `2) + (r / (sqrt 2))).[)) by TARSKI:def 2;
then A10: g . 1 in ].((p `1) - (r / (sqrt 2))),((p `1) + (r / (sqrt 2))).[ by A8, A5;
then consider m being Real such that
A11: m = g . 1 and
(p `1) - (r / (sqrt 2)) < m and
m < (p `1) + (r / (sqrt 2)) by A2;
A12: 0 <= (m - (p `1)) ^2 by XREAL_1:63;
2 in dom ((1,2) --> (].((p `1) - (r / (sqrt 2))),((p `1) + (r / (sqrt 2))).[,].((p `2) - (r / (sqrt 2))),((p `2) + (r / (sqrt 2))).[)) by A9, TARSKI:def 2;
then A13: g . 2 in ].((p `2) - (r / (sqrt 2))),((p `2) + (r / (sqrt 2))).[ by A8, A3;
then consider n being Real such that
A14: n = g . 2 and
(p `2) - (r / (sqrt 2)) < n and
n < (p `2) + (r / (sqrt 2)) by A4;
|.(n - (p `2)).| < r / (sqrt 2) by A13, A14, RCOMP_1:1;
then |.(n - (p `2)).| ^2 < (r / (sqrt 2)) ^2 by COMPLEX1:46, SQUARE_1:16;
then |.(n - (p `2)).| ^2 < (r ^2) / ((sqrt 2) ^2) by XCMPLX_1:76;
then |.(n - (p `2)).| ^2 < (r ^2) / 2 by SQUARE_1:def 2;
then A15: (n - (p `2)) ^2 < (r ^2) / 2 by COMPLEX1:75;
(p `1) - ((p `1) + (r / (sqrt 2))) < (p `1) - ((p `1) - (r / (sqrt 2))) by A10, XREAL_1:15, XXREAL_1:28;
then (- (r / (sqrt 2))) + (r / (sqrt 2)) < (r / (sqrt 2)) + (r / (sqrt 2)) by XREAL_1:6;
then A16: 0 < r by SQUARE_1:19;
A17: now :: thesis: for k being object st k in dom g holds
g . k = <*(g . 1),(g . 2)*> . k
let k be object ; :: thesis: ( k in dom g implies g . k = <*(g . 1),(g . 2)*> . k )
assume k in dom g ; :: thesis: g . k = <*(g . 1),(g . 2)*> . k
then ( k = 1 or k = 2 ) by A7, TARSKI:def 2;
hence g . k = <*(g . 1),(g . 2)*> . k by FINSEQ_1:44; :: thesis: verum
end;
A18: 0 <= (n - (p `2)) ^2 by XREAL_1:63;
|.(m - (p `1)).| < r / (sqrt 2) by A10, A11, RCOMP_1:1;
then |.(m - (p `1)).| ^2 < (r / (sqrt 2)) ^2 by COMPLEX1:46, SQUARE_1:16;
then |.(m - (p `1)).| ^2 < (r ^2) / ((sqrt 2) ^2) by XCMPLX_1:76;
then |.(m - (p `1)).| ^2 < (r ^2) / 2 by SQUARE_1:def 2;
then (m - (p `1)) ^2 < (r ^2) / 2 by COMPLEX1:75;
then ((m - (p `1)) ^2) + ((n - (p `2)) ^2) < ((r ^2) / 2) + ((r ^2) / 2) by A15, XREAL_1:8;
then sqrt (((m - (p `1)) ^2) + ((n - (p `2)) ^2)) < sqrt (r ^2) by A12, A18, SQUARE_1:27;
then A19: sqrt (((m - (p `1)) ^2) + ((n - (p `2)) ^2)) < r by A16, SQUARE_1:22;
dom <*(g . 1),(g . 2)*> = {1,2} by FINSEQ_1:2, FINSEQ_1:89;
then a = |[m,n]| by A6, A7, A11, A14, A17, FUNCT_1:2, FUNCT_4:62;
then reconsider c = a as Point of (TOP-REAL 2) ;
reconsider b = c as Point of (Euclid 2) by TOPREAL3:8;
dist (b,e) = (Pitag_dist 2) . (b,e) by METRIC_1:def 1
.= sqrt ((((c `1) - (p `1)) ^2) + (((c `2) - (p `2)) ^2)) by A1, TOPREAL3:7 ;
hence a in Ball (e,r) by A6, A11, A14, A19, METRIC_1:11; :: thesis: verum