let r be Real; :: thesis:
let n be non zero Nat; :: thesis:
let p be Element of (EMINFTY n); :: thesis:
consider x being Element of REAL n such that
A1: @ p = x ;

suppose r <= 0 ; :: thesis:

then ( Ball (p,r) = {} & product (Intervals (x,r)) = {} ) by Th67, TBSP_1:12;
hence Ball (p,r) = product (Intervals ((@ p),r)) by A1; :: thesis:

end;

suppose A2: r > 0 ; :: thesis:

A3: { q where q is Element of (EMINFTY n) : dist (p,q) < r } c= product (Intervals (x,r))

proof

let t be object ; :: according to TARSKI:def 3 :: thesis:
assume t in { q where q is Element of (EMINFTY n) : dist (p,q) < r } ; :: thesis:
then consider q being Element of (EMINFTY n) such that
A4: t = q and
A5: dist (p,q) < r ;
reconsider pr = p, qr = q as Element of REAL n ;
consider S being ext-real-membered set such that
A6: S = { |.((pr . i) - (qr . i)).| where i is Element of Seg n : verum } and
A7: (Infty_dist n) . (pr,qr) = sup S by Th57;
(Infty_dist n) . (p,q) in REAL by BINOP_1:17;
then reconsider s = (Infty_dist n) . (p,q) as Real ;
reconsider f = Intervals (x,r) as Function ;

now :: thesis:

A8: dom f = dom x by EUCLID_9:def 3
.= Seg n by FINSEQ_1:89 ;
hence dom qr = dom f by FINSEQ_1:89; :: thesis:
thus for y being object st y in dom f holds
qr . y in f . y :: thesis:

proof

let y be object ; :: thesis:
assume A9: y in dom f ; :: thesis:
then A10: y in dom x by A8, FINSEQ_1:89;
reconsider y1 = y as Element of Seg n by A9, A8;
|.((pr . y1) - (qr . y1)).| in S by A6;
then ( |.((pr . y1) - (qr . y1)).| <= sup S & sup S < r ) by A7, A5, XXREAL_2:4;
then A11: |.((x . y) - (qr . y)).| < r by A1, XXREAL_0:2;
( (x . y) - r < qr . y & qr . y < (x . y) + r )

proof

per cases ) - (qr . y) >= 0 or (x . y) - (qr . y) < 0 ) ;

suppose A12: (x . y) - (qr . y) >= 0 ; :: thesis:

then (x . y) - (qr . y) < r by A11, COMPLEX1:43;
then ((x . y) - (qr . y)) + (qr . y) < (qr . y) + r by XREAL_1:8;
then (x . y) - r < ((qr . y) + r) - r by XREAL_1:8;
hence (x . y) - r < qr . y ; :: thesis:
0 + (qr . y) <= ((x . y) - (qr . y)) + (qr . y) by A12, XREAL_1:7;
hence qr . y < (x . y) + r by A2, XREAL_1:8; :: thesis:

end;

suppose A13: (x . y) - (qr . y) < 0 ; :: thesis:

then ((x . y) - (qr . y)) + (qr . y) < 0 + (qr . y) by XREAL_1:8;
then (x . y) - r < (qr . y) - 0 by A2, XREAL_1:15;
hence (x . y) - r < qr . y ; :: thesis:
|.((x . y) - (qr . y)).| = - ((x . y) - (qr . y)) by A13, COMPLEX1:70
.= (qr . y) - (x . y) ;
then ((qr . y) - (x . y)) + (x . y) < r + (x . y) by A11, XREAL_1:8;
hence qr . y < (x . y) + r ; :: thesis:

end;

then qr . y in ].((x . y) - r),((x . y) + r).[ by XXREAL_1:4;
hence qr . y in f . y by A10, EUCLID_9:def 3; :: thesis:

end;

hence t in product (Intervals (x,r)) by A4, CARD_3:9; :: thesis:

end;

product (Intervals (x,r)) c= { q where q is Element of (EMINFTY n) : dist (p,q) < r }

proof

let t be object ; :: according to TARSKI:def 3 :: thesis:
assume t in product (Intervals (x,r)) ; :: thesis:
then consider g being Function such that
A14: t = g and
A15: dom g = dom (Intervals (x,r)) and
A16: for y being object st y in dom (Intervals (x,r)) holds
g . y in (Intervals (x,r)) . y by CARD_3:def 5;
A17: dom (Intervals (x,r)) = dom x by EUCLID_9:def 3
.= Seg n by FINSEQ_1:89 ;
rng g c= REAL

proof

let u be object ; :: according to TARSKI:def 3 :: thesis:
assume u in rng g ; :: thesis:
then consider t being object such that
A18: t in dom g and
A19: u = g . t by FUNCT_1:def 3;
A20: u in (Intervals (x,r)) . t by A18, A19, A15, A16;
t in dom x by A18, A17, A15, FINSEQ_1:89;
then u in ].((x . t) - r),((x . t) + r).[ by A20, EUCLID_9:def 3;
hence u in REAL ; :: thesis:

end;

then g in Funcs ((Seg n),REAL) by A17, A15, FUNCT_2:def 2;
then reconsider g0 = g as Element of (EMINFTY n) by FINSEQ_2:93;
dist (p,g0) < r

proof

reconsider p1 = p, g1 = g0 as Element of REAL n ;
consider S being ext-real-membered set such that
S = { |.((p1 . i) - (g1 . i)).| where i is Element of Seg n : verum } and
A21: (Infty_dist n) . (p1,g1) = sup S by Th57;
sup S < r

proof

proof

per cases ) . (max_diff_index (p1,g1)) < 0 or 0 <= (p1 - g1) . (max_diff_index (p1,g1)) ) ;

suppose (p1 - g1) . (max_diff_index (p1,g1)) < 0 ; :: thesis:

then |.((p1 - g1) . (max_diff_index (p1,g1))).| = - ((p1 - g1) . (max_diff_index (p1,g1))) by COMPLEX1:70;
hence |.((p1 - g1) . (max_diff_index (p1,g1))).| < r by A28, RVSUM_1:27; :: thesis:

end;

suppose 0 <= (p1 - g1) . (max_diff_index (p1,g1)) ; :: thesis:

hence |.((p1 - g1) . (max_diff_index (p1,g1))).| < r by A29, COMPLEX1:43; :: thesis:

end;

hence contradiction by A23, VALUED_1:18; :: thesis:

end;

hence dist (p,g0) < r by A21; :: thesis:

end;

hence t in { q where q is Element of (EMINFTY n) : dist (p,q) < r } by A14; :: thesis:

end;

hence Ball (p,r) = product (Intervals ((@ p),r)) by A1, A3, METRIC_1:def 14; :: thesis:

end;