let p be Point of (TOP-REAL 2); :: thesis: for e being Point of (Euclid 2)
for r being Real st p = e holds
Ball (e,r) c= product ((1,2) --> (].((p `1) - r),((p `1) + r).[,].((p `2) - r),((p `2) + r).[))
let e be Point of (Euclid 2); :: thesis: for r being Real st p = e holds
Ball (e,r) c= product ((1,2) --> (].((p `1) - r),((p `1) + r).[,].((p `2) - r),((p `2) + r).[))
let r be Real; :: thesis: ( p = e implies Ball (e,r) c= product ((1,2) --> (].((p `1) - r),((p `1) + r).[,].((p `2) - r),((p `2) + r).[)) )
set A = ].((p `1) - r),((p `1) + r).[;
set B = ].((p `2) - r),((p `2) + r).[;
set f = (1,2) --> (].((p `1) - r),((p `1) + r).[,].((p `2) - r),((p `2) + r).[);
assume A1: p = e ; :: thesis: Ball (e,r) c= product ((1,2) --> (].((p `1) - r),((p `1) + r).[,].((p `2) - r),((p `2) + r).[))
let a be object ; :: according to TARSKI:def 3 :: thesis: ( not a in Ball (e,r) or a in product ((1,2) --> (].((p `1) - r),((p `1) + r).[,].((p `2) - r),((p `2) + r).[)) )
assume A2: a in Ball (e,r) ; :: thesis: a in product ((1,2) --> (].((p `1) - r),((p `1) + r).[,].((p `2) - r),((p `2) + r).[))
then reconsider b = a as Point of (Euclid 2) ;
reconsider q = b as Point of (TOP-REAL 2) by TOPREAL3:8;
reconsider g = q as FinSequence ;
A3: for x being object st x in dom ((1,2) --> (].((p `1) - r),((p `1) + r).[,].((p `2) - r),((p `2) + r).[)) holds
g . x in ((1,2) --> (].((p `1) - r),((p `1) + r).[,].((p `2) - r),((p `2) + r).[)) . x

proof

let x be object ; :: thesis: ( x in dom ((1,2) --> (].((p `1) - r),((p `1) + r).[,].((p `2) - r),((p `2) + r).[)) implies g . x in ((1,2) --> (].((p `1) - r),((p `1) + r).[,].((p `2) - r),((p `2) + r).[)) . x )
assume A4: x in dom ((1,2) --> (].((p `1) - r),((p `1) + r).[,].((p `2) - r),((p `2) + r).[)) ; :: thesis: g . x in ((1,2) --> (].((p `1) - r),((p `1) + r).[,].((p `2) - r),((p `2) + r).[)) . x

per cases ( x = 1 or x = 2 ) by A4, TARSKI:def 2;

suppose A5: x = 1 ; :: thesis: g . x in ((1,2) --> (].((p `1) - r),((p `1) + r).[,].((p `2) - r),((p `2) + r).[)) . x

A6: ((1,2) --> (].((p `1) - r),((p `1) + r).[,].((p `2) - r),((p `2) + r).[)) . 1 = ].((p `1) - r),((p `1) + r).[ by FUNCT_4:63;
A7: q `1 < (p `1) + r by A1, A2, Th37;
(p `1) - r < q `1 by A1, A2, Th37;
hence g . x in ((1,2) --> (].((p `1) - r),((p `1) + r).[,].((p `2) - r),((p `2) + r).[)) . x by A5, A6, A7, XXREAL_1:4; :: thesis: verum

end;

suppose A8: x = 2 ; :: thesis: g . x in ((1,2) --> (].((p `1) - r),((p `1) + r).[,].((p `2) - r),((p `2) + r).[)) . x

A9: ((1,2) --> (].((p `1) - r),((p `1) + r).[,].((p `2) - r),((p `2) + r).[)) . 2 = ].((p `2) - r),((p `2) + r).[ by FUNCT_4:63;
A10: q `2 < (p `2) + r by A1, A2, Th38;
(p `2) - r < q `2 by A1, A2, Th38;
hence g . x in ((1,2) --> (].((p `1) - r),((p `1) + r).[,].((p `2) - r),((p `2) + r).[)) . x by A8, A9, A10, XXREAL_1:4; :: thesis: verum

end;

end;

end;

q is Function of (Seg 2),REAL by EUCLID:23;
then A11: dom g = {1,2} by FINSEQ_1:2, FUNCT_2:def 1;
dom ((1,2) --> (].((p `1) - r),((p `1) + r).[,].((p `2) - r),((p `2) + r).[)) = {1,2} by FUNCT_4:62;
hence a in product ((1,2) --> (].((p `1) - r),((p `1) + r).[,].((p `2) - r),((p `2) + r).[)) by A11, A3, CARD_3:9; :: thesis: verum