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
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 number 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 number ; :: 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 set ; :: 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:13;
reconsider g = q as FinSequence ;
A3: for x being set 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 set ; :: 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:66;
A7: q `1 < (p `1 ) + r by A1, A2, Th47;
(p `1 ) - r < q `1 by A1, A2, Th47;
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:66;
A10: q `2 < (p `2 ) + r by A1, A2, Th48;
(p `2 ) - r < q `2 by A1, A2, Th48;
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:26;
then A11: dom g = {1,2} by FINSEQ_1:4, FUNCT_2:def 1;
dom (1,2 --> ].((p `1 ) - r),((p `1 ) + r).[,].((p `2 ) - r),((p `2 ) + r).[) = {1,2} by FUNCT_4:65;
hence a in product (1,2 --> ].((p `1 ) - r),((p `1 ) + r).[,].((p `2 ) - r),((p `2 ) + r).[) by A11, A3, CARD_3:18; :: thesis: verum