let n be Nat; :: thesis: for r being Real

for e being Point of (Euclid n) holds Ball (e,r) c= OpenHypercube (e,r)

let r be Real; :: thesis: for e being Point of (Euclid n) holds Ball (e,r) c= OpenHypercube (e,r)

let e be Point of (Euclid n); :: thesis: Ball (e,r) c= OpenHypercube (e,r)

let g be object ; :: according to TARSKI:def 3 :: thesis: ( not g in Ball (e,r) or g in OpenHypercube (e,r) )

assume A1: g in Ball (e,r) ; :: thesis: g in OpenHypercube (e,r)

then reconsider g = g as Point of (Euclid n) ;

A2: dom (Intervals (e,r)) = dom e by Def3;

A3: ( dom g = Seg n & dom e = Seg n ) by FINSEQ_1:89;

for e being Point of (Euclid n) holds Ball (e,r) c= OpenHypercube (e,r)

let r be Real; :: thesis: for e being Point of (Euclid n) holds Ball (e,r) c= OpenHypercube (e,r)

let e be Point of (Euclid n); :: thesis: Ball (e,r) c= OpenHypercube (e,r)

let g be object ; :: according to TARSKI:def 3 :: thesis: ( not g in Ball (e,r) or g in OpenHypercube (e,r) )

assume A1: g in Ball (e,r) ; :: thesis: g in OpenHypercube (e,r)

then reconsider g = g as Point of (Euclid n) ;

A2: dom (Intervals (e,r)) = dom e by Def3;

A3: ( dom g = Seg n & dom e = Seg n ) by FINSEQ_1:89;

now :: thesis: for x being object st x in dom (Intervals (e,r)) holds

g . x in (Intervals (e,r)) . x

hence
g in OpenHypercube (e,r)
by A2, A3, CARD_3:9; :: thesis: verumg . x in (Intervals (e,r)) . x

let x be object ; :: thesis: ( x in dom (Intervals (e,r)) implies g . x in (Intervals (e,r)) . x )

reconsider u = e . x, v = g . x as Real ;

assume A4: x in dom (Intervals (e,r)) ; :: thesis: g . x in (Intervals (e,r)) . x

then A5: (Intervals (e,r)) . x = ].(u - r),(u + r).[ by A2, Def3;

dom (g - e) = (dom g) /\ (dom e) by VALUED_1:12;

then A6: (g - e) . x = v - u by A2, A3, A4, VALUED_1:13;

A7: v = u + (v - u) ;

|.((g - e) . x).| < r by A1, Th10;

hence g . x in (Intervals (e,r)) . x by A6, A5, A7, FCONT_3:3; :: thesis: verum

end;reconsider u = e . x, v = g . x as Real ;

assume A4: x in dom (Intervals (e,r)) ; :: thesis: g . x in (Intervals (e,r)) . x

then A5: (Intervals (e,r)) . x = ].(u - r),(u + r).[ by A2, Def3;

dom (g - e) = (dom g) /\ (dom e) by VALUED_1:12;

then A6: (g - e) . x = v - u by A2, A3, A4, VALUED_1:13;

A7: v = u + (v - u) ;

|.((g - e) . x).| < r by A1, Th10;

hence g . x in (Intervals (e,r)) . x by A6, A5, A7, FCONT_3:3; :: thesis: verum