let r be Real; :: thesis: for p being Point of (TOP-REAL 3)
for e being Point of (Euclid 3) st p = e & p `3 = 0 holds
product ((1,2,3) --> (].((p `1) - (r / (sqrt 2))),((p `1) + (r / (sqrt 2))).[,].((p `2) - (r / (sqrt 2))),((p `2) + (r / (sqrt 2))).[,{0})) c= Ball (e,r)
let p be Point of (TOP-REAL 3); :: thesis: for e being Point of (Euclid 3) st p = e & p `3 = 0 holds
product ((1,2,3) --> (].((p `1) - (r / (sqrt 2))),((p `1) + (r / (sqrt 2))).[,].((p `2) - (r / (sqrt 2))),((p `2) + (r / (sqrt 2))).[,{0})) c= Ball (e,r)
let e be Point of (Euclid 3); :: thesis: ( p = e & p `3 = 0 implies product ((1,2,3) --> (].((p `1) - (r / (sqrt 2))),((p `1) + (r / (sqrt 2))).[,].((p `2) - (r / (sqrt 2))),((p `2) + (r / (sqrt 2))).[,{0})) 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 C = {0};
set f = (1,2,3) --> (].((p `1) - (r / (sqrt 2))),((p `1) + (r / (sqrt 2))).[,].((p `2) - (r / (sqrt 2))),((p `2) + (r / (sqrt 2))).[,{0});
assume that
A1: p = e and
A2: p `3 = 0 ; :: thesis: product ((1,2,3) --> (].((p `1) - (r / (sqrt 2))),((p `1) + (r / (sqrt 2))).[,].((p `2) - (r / (sqrt 2))),((p `2) + (r / (sqrt 2))).[,{0})) c= Ball (e,r)
let a be object ; :: according to TARSKI:def 3 :: thesis: ( not a in product ((1,2,3) --> (].((p `1) - (r / (sqrt 2))),((p `1) + (r / (sqrt 2))).[,].((p `2) - (r / (sqrt 2))),((p `2) + (r / (sqrt 2))).[,{0})) or a in Ball (e,r) )
assume a in product ((1,2,3) --> (].((p `1) - (r / (sqrt 2))),((p `1) + (r / (sqrt 2))).[,].((p `2) - (r / (sqrt 2))),((p `2) + (r / (sqrt 2))).[,{0})) ; :: thesis: a in Ball (e,r)
then consider g being Function such that
A3: a = g and
A4: dom g = dom ((1,2,3) --> (].((p `1) - (r / (sqrt 2))),((p `1) + (r / (sqrt 2))).[,].((p `2) - (r / (sqrt 2))),((p `2) + (r / (sqrt 2))).[,{0})) and
A5: for x being object st x in dom ((1,2,3) --> (].((p `1) - (r / (sqrt 2))),((p `1) + (r / (sqrt 2))).[,].((p `2) - (r / (sqrt 2))),((p `2) + (r / (sqrt 2))).[,{0})) holds
g . x in ((1,2,3) --> (].((p `1) - (r / (sqrt 2))),((p `1) + (r / (sqrt 2))).[,].((p `2) - (r / (sqrt 2))),((p `2) + (r / (sqrt 2))).[,{0})) . x by CARD_3:def 5;
A6: ].((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;
A7: ].((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;
A8: dom ((1,2,3) --> (].((p `1) - (r / (sqrt 2))),((p `1) + (r / (sqrt 2))).[,].((p `2) - (r / (sqrt 2))),((p `2) + (r / (sqrt 2))).[,{0})) = {1,2,3} by FUNCT_4:128;
then A9: ( 1 in dom ((1,2,3) --> (].((p `1) - (r / (sqrt 2))),((p `1) + (r / (sqrt 2))).[,].((p `2) - (r / (sqrt 2))),((p `2) + (r / (sqrt 2))).[,{0})) & 2 in dom ((1,2,3) --> (].((p `1) - (r / (sqrt 2))),((p `1) + (r / (sqrt 2))).[,].((p `2) - (r / (sqrt 2))),((p `2) + (r / (sqrt 2))).[,{0})) & 3 in dom ((1,2,3) --> (].((p `1) - (r / (sqrt 2))),((p `1) + (r / (sqrt 2))).[,].((p `2) - (r / (sqrt 2))),((p `2) + (r / (sqrt 2))).[,{0})) ) by ENUMSET1:def 1;
A10: ( ((1,2,3) --> (].((p `1) - (r / (sqrt 2))),((p `1) + (r / (sqrt 2))).[,].((p `2) - (r / (sqrt 2))),((p `2) + (r / (sqrt 2))).[,{0})) . 1 = ].((p `1) - (r / (sqrt 2))),((p `1) + (r / (sqrt 2))).[ & ((1,2,3) --> (].((p `1) - (r / (sqrt 2))),((p `1) + (r / (sqrt 2))).[,].((p `2) - (r / (sqrt 2))),((p `2) + (r / (sqrt 2))).[,{0})) . 2 = ].((p `2) - (r / (sqrt 2))),((p `2) + (r / (sqrt 2))).[ & ((1,2,3) --> (].((p `1) - (r / (sqrt 2))),((p `1) + (r / (sqrt 2))).[,].((p `2) - (r / (sqrt 2))),((p `2) + (r / (sqrt 2))).[,{0})) . 3 = {0} ) by FUNCT_4:135, FUNCT_4:134;
then A11: ( g . 1 in ].((p `1) - (r / (sqrt 2))),((p `1) + (r / (sqrt 2))).[ & g . 2 in ].((p `2) - (r / (sqrt 2))),((p `2) + (r / (sqrt 2))).[ & g . 3 in {0} ) by A5, A9;
then consider m being Real such that
A12: m = g . 1 and
( (p `1) - (r / (sqrt 2)) < m & m < (p `1) + (r / (sqrt 2)) ) by A6;
consider n being Real such that
A13: n = g . 2 and
( (p `2) - (r / (sqrt 2)) < n & n < (p `2) + (r / (sqrt 2)) ) by A7, A11;
g . 3 in ((1,2,3) --> (].((p `1) - (r / (sqrt 2))),((p `1) + (r / (sqrt 2))).[,].((p `2) - (r / (sqrt 2))),((p `2) + (r / (sqrt 2))).[,{0})) . 3 by A5, A9;
then A14: g . 3 = 0 by A10, TARSKI:def 1;
(p `1) + (r / (sqrt 2)) > (p `1) - (r / (sqrt 2)) by A11, XXREAL_1:28;
then (p `1) - ((p `1) + (r / (sqrt 2))) < (p `1) - ((p `1) - (r / (sqrt 2))) by XREAL_1:10;
then (- (r / (sqrt 2))) + (r / (sqrt 2)) < (r / (sqrt 2)) + (r / (sqrt 2)) by XREAL_1:6;
then A15: 0 < r ;
A16: dom <*(g . 1),(g . 2),(g . 3)*> = Seg (len <*(g . 1),(g . 2),(g . 3)*>) by FINSEQ_1:def 3
.= {1,2,3} by FINSEQ_1:45, FINSEQ_3:1 ;

now :: thesis: for k being object st k in dom g holds
g . k = <*(g . 1),(g . 2),(g . 3)*> . k

let k be object ; :: thesis: ( k in dom g implies g . k = <*(g . 1),(g . 2),(g . 3)*> . k )
assume k in dom g ; :: thesis: g . k = <*(g . 1),(g . 2),(g . 3)*> . k
then ( k = 1 or k = 2 or k = 3 ) by A4, A8, ENUMSET1:def 1;
hence g . k = <*(g . 1),(g . 2),(g . 3)*> . k ; :: thesis: verum

end;

then A17: a = |[m,n,0]| by A3, A4, A12, A13, A16, A14, FUNCT_4:128, FUNCT_1:2;
then reconsider c = a as Point of (TOP-REAL 3) ;
reconsider b = c as Point of (Euclid 3) by TOPREAL3:8;
( |.(m - (p `1)).| < r / (sqrt 2) & |.(n - (p `2)).| < r / (sqrt 2) ) by A11, A12, A13, RCOMP_1:1;
then ( |.(m - (p `1)).| ^2 < (r / (sqrt 2)) ^2 & |.(n - (p `2)).| ^2 < (r / (sqrt 2)) ^2 ) by SQUARE_1:16;
then ( |.(m - (p `1)).| ^2 < (r ^2) / ((sqrt 2) ^2) & |.(n - (p `2)).| ^2 < (r ^2) / ((sqrt 2) ^2) ) by XCMPLX_1:76;
then ( |.(m - (p `1)).| ^2 < (r ^2) / 2 & |.(n - (p `2)).| ^2 < (r ^2) / 2 ) by SQUARE_1:def 2;
then ( (m - (p `1)) ^2 < (r ^2) / 2 & (n - (p `2)) ^2 < (r ^2) / 2 ) by COMPLEX1:75;
then ((m - (p `1)) ^2) + ((n - (p `2)) ^2) < ((r ^2) / 2) + ((r ^2) / 2) by XREAL_1:8;
then sqrt (((m - (p `1)) ^2) + ((n - (p `2)) ^2)) < sqrt (r ^2) by SQUARE_1:27;
then A18: sqrt (((m - (p `1)) ^2) + ((n - (p `2)) ^2)) < r by A15, SQUARE_1:22;
A19: ( m = c `1 & n = c `2 ) by A17, EUCLID_5:2;
dist (b,e) = (Pitag_dist 3) . (b,e) by METRIC_1:def 1
.= sqrt (((((c `1) - (p `1)) ^2) + (((c `2) - (p `2)) ^2)) + (((c `3) - (p `3)) ^2)) by A1, Th37
.= sqrt (((((c `1) - (p `1)) ^2) + (((c `2) - (p `2)) ^2)) + ((Q - Q) ^2)) by A2, A17, EUCLID_5:2
.= sqrt (((((c `1) - (p `1)) ^2) + (((c `2) - (p `2)) ^2)) + Q) ;
hence a in Ball (e,r) by A18, A19, METRIC_1:11; :: thesis: verum