let r be Real; :: thesis: for n being non zero Nat
for p being Element of (EMINFTY n)
for t being object holds
( t in cl_Ball (p,r) iff ex f being Function st
( t = f & dom f = Seg n & ( for i being Nat st i in Seg n holds
f . i in [.(((@ p) . i) - r),(((@ p) . i) + r).] ) ) )
let n be non zero Nat; :: thesis: for p being Element of (EMINFTY n)
for t being object holds
( t in cl_Ball (p,r) iff ex f being Function st
( t = f & dom f = Seg n & ( for i being Nat st i in Seg n holds
f . i in [.(((@ p) . i) - r),(((@ p) . i) + r).] ) ) )
let p be Element of (EMINFTY n); :: thesis: for t being object holds
( t in cl_Ball (p,r) iff ex f being Function st
( t = f & dom f = Seg n & ( for i being Nat st i in Seg n holds
f . i in [.(((@ p) . i) - r),(((@ p) . i) + r).] ) ) )
reconsider x = @ p as Element of REAL n ;

per cases ( r < 0 or 0 <= r ) ;

suppose A1: r < 0 ; :: thesis: for t being object holds
( t in cl_Ball (p,r) iff ex f being Function st
( t = f & dom f = Seg n & ( for i being Nat st i in Seg n holds
f . i in [.(((@ p) . i) - r),(((@ p) . i) + r).] ) ) )

for t being object st ex f being Function st
( t = f & dom f = Seg n & ( for i being Nat st i in Seg n holds
f . i in [.((x . i) - r),((x . i) + r).] ) ) holds
t in cl_Ball (p,r)

proof

let t be object ; :: thesis: ( ex f being Function st
( t = f & dom f = Seg n & ( for i being Nat st i in Seg n holds
f . i in [.((x . i) - r),((x . i) + r).] ) ) implies t in cl_Ball (p,r) )
given f being Function such that t = f and
dom f = Seg n and
A2: for i being Nat st i in Seg n holds
f . i in [.((x . i) - r),((x . i) + r).] ; :: thesis: t in cl_Ball (p,r)
( (x . 1) + r < x . 1 & x . 1 < (x . 1) - r ) by A1, XREAL_1:30, XREAL_1:46;
then (x . 1) + r < (x . 1) - r by XXREAL_0:2;
then A3: [.((x . 1) - r),((x . 1) + r).] is empty by XXREAL_1:29;
0 + 1 < n + 1 by XREAL_1:6;
then 1 <= n by NAT_1:13;
then 1 in Seg n ;
hence t in cl_Ball (p,r) by A3, A2; :: thesis: verum

end;

hence for t being object holds
( t in cl_Ball (p,r) iff ex f being Function st
( t = f & dom f = Seg n & ( for i being Nat st i in Seg n holds
f . i in [.(((@ p) . i) - r),(((@ p) . i) + r).] ) ) ) by A1; :: thesis: verum

end;

suppose A4: 0 <= r ; :: thesis: for t being object holds
( t in cl_Ball (p,r) iff ex f being Function st
( t = f & dom f = Seg n & ( for i being Nat st i in Seg n holds
f . i in [.(((@ p) . i) - r),(((@ p) . i) + r).] ) ) )

A5: for t being object st t in cl_Ball (p,r) holds
ex f being Function st
( t = f & dom f = Seg n & ( for i being Nat st i in Seg n holds
f . i in [.((x . i) - r),((x . i) + r).] ) )

proof

let t be object ; :: thesis: ( t in cl_Ball (p,r) implies ex f being Function st
( t = f & dom f = Seg n & ( for i being Nat st i in Seg n holds
f . i in [.((x . i) - r),((x . i) + r).] ) ) )
assume A6: t in cl_Ball (p,r) ; :: thesis: ex f being Function st
( t = f & dom f = Seg n & ( for i being Nat st i in Seg n holds
f . i in [.((x . i) - r),((x . i) + r).] ) )
reconsider f = t as Function by A6;
take f ; :: thesis: ( t = f & dom f = Seg n & ( for i being Nat st i in Seg n holds
f . i in [.((x . i) - r),((x . i) + r).] ) )
thus t = f ; :: thesis: ( dom f = Seg n & ( for i being Nat st i in Seg n holds
f . i in [.((x . i) - r),((x . i) + r).] ) )
f is Tuple of n, REAL by A6, FINSEQ_2:131;
hence dom f = Seg n by FINSEQ_2:124; :: thesis: for i being Nat st i in Seg n holds
f . i in [.((x . i) - r),((x . i) + r).]

hereby :: thesis: verum

let i be Nat; :: thesis: ( i in Seg n implies f . i in [.((x . i) - r),((x . i) + r).] )
assume A7: i in Seg n ; :: thesis: f . i in [.((x . i) - r),((x . i) + r).]
reconsider fx = t as Element of (EMINFTY n) by A6;
A8: dist (fx,p) <= r by A6, METRIC_1:12;
reconsider rfx = fx, rp = p as Element of REAL n ;
consider S being ext-real-membered set such that
A9: S = { |.((rfx . i) - (rp . i)).| where i is Element of Seg n : verum } and
A10: (Infty_dist n) . (rfx,rp) = sup S by Th57;
|.((rfx . i) - (rp . i)).| in S by A9, A7;
then |.((rfx . i) - (rp . i)).| <= sup S by XXREAL_2:4;
then A11: |.((rfx . i) - (rp . i)).| <= r by A10, A8, XXREAL_0:2;
set rfp = (rfx . i) - (rp . i);
( (x . i) - r <= rfx . i & rfx . i <= (x . i) + r )

proof

per cases ( 0 <= (rfx . i) - (rp . i) or (rfx . i) - (rp . i) < 0 ) ;

suppose A12: 0 <= (rfx . i) - (rp . i) ; :: thesis: ( (x . i) - r <= rfx . i & rfx . i <= (x . i) + r )

then (rfx . i) - (rp . i) <= r by A11, COMPLEX1:43;
then A13: ((rfx . i) - (rp . i)) + (rp . i) <= r + (rp . i) by XREAL_1:7;
0 + (rp . i) <= ((rfx . i) - (rp . i)) + (rp . i) by A12, XREAL_1:7;
then ( (rp . i) - r <= (rfx . i) - r & (rfx . i) - r <= rfx . i ) by A4, XREAL_1:13, XREAL_1:43;
hence ( (x . i) - r <= rfx . i & rfx . i <= (x . i) + r ) by A13, XXREAL_0:2; :: thesis: verum

end;

suppose A14: (rfx . i) - (rp . i) < 0 ; :: thesis: ( (x . i) - r <= rfx . i & rfx . i <= (x . i) + r )

then - ((rfx . i) - (rp . i)) <= r by A11, COMPLEX1:70;
then ((rp . i) - (rfx . i)) + (rfx . i) <= r + (rfx . i) by XREAL_1:7;
then (rp . i) - r <= (r + (rfx . i)) - r by XREAL_1:13;
hence (x . i) - r <= rfx . i ; :: thesis: rfx . i <= (x . i) + r
((rfx . i) - (rp . i)) + (rp . i) < 0 + (rp . i) by A14, XREAL_1:8;
hence rfx . i <= (x . i) + r by A4, XREAL_1:38; :: thesis: verum

end;

end;

end;

hence f . i in [.((x . i) - r),((x . i) + r).] by XXREAL_1:1; :: thesis: verum

end;

end;

for t being object st ex f being Function st
( t = f & dom f = Seg n & ( for i being Nat st i in Seg n holds
f . i in [.((x . i) - r),((x . i) + r).] ) ) holds
t in cl_Ball (p,r)

proof

let t be object ; :: thesis: ( ex f being Function st
( t = f & dom f = Seg n & ( for i being Nat st i in Seg n holds
f . i in [.((x . i) - r),((x . i) + r).] ) ) implies t in cl_Ball (p,r) )
assume A15: ex f being Function st
( t = f & dom f = Seg n & ( for i being Nat st i in Seg n holds
f . i in [.((x . i) - r),((x . i) + r).] ) ) ; :: thesis: t in cl_Ball (p,r)
then consider f being Function such that
A16: t = f and
A17: dom f = Seg n and
A18: for i being Nat st i in Seg n holds
f . i in [.((x . i) - r),((x . i) + r).] ;
rng f c= REAL

proof

let u be object ; :: according to TARSKI:def 3 :: thesis: ( not u in rng f or u in REAL )
assume u in rng f ; :: thesis: u in REAL
then consider v being object such that
A19: v in dom f and
A20: u = f . v by FUNCT_1:def 3;
f . v in [.((x . v) - r),((x . v) + r).] by A19, A17, A18;
hence u in REAL by A20; :: thesis: verum

end;

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

proof

reconsider rp = p, rq = q as Element of REAL n ;
consider S being ext-real-membered set such that
A21: S = { |.((rp . i) - (rq . i)).| where i is Element of Seg n : verum } and
A22: (Infty_dist n) . (rp,rq) = sup S by Th57;
for e being ExtReal st e in S holds
e <= r

proof

let e be ExtReal; :: thesis: ( e in S implies e <= r )
assume e in S ; :: thesis: e <= r
then consider i being Element of Seg n such that
A23: e = |.((rp . i) - (rq . i)).| by A21;
|.((rp . i) - (rq . i)).| <= r

proof

rq . i in [.((rp . i) - r),((rp . i) + r).] by A16, A15;
then A24: ( (rp . i) - r <= rq . i & rq . i <= (rp . i) + r ) by XXREAL_1:1;
set rpq = (rp . i) - (rq . i);

per cases ( 0 <= (rp . i) - (rq . i) or (rp . i) - (rq . i) < 0 ) ;

suppose A25: 0 <= (rp . i) - (rq . i) ; :: thesis: |.((rp . i) - (rq . i)).| <= r

(rp . i) - (rq . i) <= r

proof

((rp . i) - r) + r <= (rq . i) + r by A24, XREAL_1:7;
then (rp . i) - (rq . i) <= ((rq . i) + r) - (rq . i) by XREAL_1:13;
hence (rp . i) - (rq . i) <= r ; :: thesis: verum

end;

hence |.((rp . i) - (rq . i)).| <= r by A25, COMPLEX1:43; :: thesis: verum

end;

suppose A26: (rp . i) - (rq . i) < 0 ; :: thesis: |.((rp . i) - (rq . i)).| <= r

- ((rp . i) - (rq . i)) <= r

proof

(rq . i) - (rp . i) <= ((rp . i) + r) - (rp . i) by A24, XREAL_1:13;
hence - ((rp . i) - (rq . i)) <= r ; :: thesis: verum

end;

hence |.((rp . i) - (rq . i)).| <= r by A26, COMPLEX1:70; :: thesis: verum

end;

end;

end;

hence e <= r by A23; :: thesis: verum

end;

then r is UpperBound of S by XXREAL_2:def 1;
hence dist (p,q) <= r by A22, XXREAL_2:def 3; :: thesis: verum

end;

hence t in cl_Ball (p,r) by A16, METRIC_1:12; :: thesis: verum

end;

hence for t being object holds
( t in cl_Ball (p,r) iff ex f being Function st
( t = f & dom f = Seg n & ( for i being Nat st i in Seg n holds
f . i in [.(((@ p) . i) - r),(((@ p) . i) + r).] ) ) ) by A5; :: thesis: verum

end;

end;