let p be Point of (TOP-REAL 2); :: thesis: for e being Point of (Euclid 2)
for r being real number 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 number 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 number ; :: 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 set ; :: 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:66;
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:66;
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 set 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:65;
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:65;
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;
abs (n - (p `2 )) < r / (sqrt 2) by A13, A14, RCOMP_1:8;
then (abs (n - (p `2 ))) ^2 < (r / (sqrt 2)) ^2 by COMPLEX1:132, SQUARE_1:78;
then (abs (n - (p `2 ))) ^2 < (r ^2 ) / ((sqrt 2) ^2 ) by XCMPLX_1:77;
then (abs (n - (p `2 ))) ^2 < (r ^2 ) / 2 by SQUARE_1:def 4;
then A15: (n - (p `2 )) ^2 < (r ^2 ) / 2 by COMPLEX1:161;
(p `1 ) - ((p `1 ) + (r / (sqrt 2))) < (p `1 ) - ((p `1 ) - (r / (sqrt 2))) by A10, XREAL_1:17, XXREAL_1:28;
then (- (r / (sqrt 2))) + (r / (sqrt 2)) < (r / (sqrt 2)) + (r / (sqrt 2)) by XREAL_1:8;
then A16: 0 < r by SQUARE_1:84;

A17: now

let k be set ; :: 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:61; :: thesis: verum

end;

A18: 0 <= (n - (p `2 )) ^2 by XREAL_1:65;
abs (m - (p `1 )) < r / (sqrt 2) by A10, A11, RCOMP_1:8;
then (abs (m - (p `1 ))) ^2 < (r / (sqrt 2)) ^2 by COMPLEX1:132, SQUARE_1:78;
then (abs (m - (p `1 ))) ^2 < (r ^2 ) / ((sqrt 2) ^2 ) by XCMPLX_1:77;
then (abs (m - (p `1 ))) ^2 < (r ^2 ) / 2 by SQUARE_1:def 4;
then (m - (p `1 )) ^2 < (r ^2 ) / 2 by COMPLEX1:161;
then ((m - (p `1 )) ^2 ) + ((n - (p `2 )) ^2 ) < ((r ^2 ) / 2) + ((r ^2 ) / 2) by A15, XREAL_1:10;
then sqrt (((m - (p `1 )) ^2 ) + ((n - (p `2 )) ^2 )) < sqrt (r ^2 ) by A12, A18, SQUARE_1:95;
then A19: sqrt (((m - (p `1 )) ^2 ) + ((n - (p `2 )) ^2 )) < r by A16, SQUARE_1:89;
dom <*(g . 1),(g . 2)*> = {1,2} by FINSEQ_1:4, FINSEQ_3:29;
then a = |[m,n]| by A6, A7, A11, A14, A17, FUNCT_1:9, FUNCT_4:65;
then reconsider c = a as Point of (TOP-REAL 2) ;
reconsider b = c as Point of (Euclid 2) by TOPREAL3:13;
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:12 ;
hence a in Ball e,r by A6, A11, A14, A19, METRIC_1:12; :: thesis: verum