let n be Nat; :: thesis: for r being real number
for e1, e being Point of (Euclid n) st ( n <> 0 or 0 < r ) & e1 in OpenHypercube (e,r) holds
for x being set holds
( abs ((e1 - e) . x) < r & abs ((e1 . x) - (e . x)) < r )
let r be real number ; :: thesis: for e1, e being Point of (Euclid n) st ( n <> 0 or 0 < r ) & e1 in OpenHypercube (e,r) holds
for x being set holds
( abs ((e1 - e) . x) < r & abs ((e1 . x) - (e . x)) < r )
let e1, e be Point of (Euclid n); :: thesis: ( ( n <> 0 or 0 < r ) & e1 in OpenHypercube (e,r) implies for x being set holds
( abs ((e1 - e) . x) < r & abs ((e1 . x) - (e . x)) < r ) )
assume that
A1: ( n <> 0 or 0 < r ) and
A2: e1 in OpenHypercube (e,r) ; :: thesis: for x being set holds
( abs ((e1 - e) . x) < r & abs ((e1 . x) - (e . x)) < r )
A3: ( dom e1 = Seg n & dom e = Seg n ) by EUCLID:3;
A4: dom (e1 - e) = (dom e1) /\ (dom e) by VALUED_1:12;
let x be set ; :: thesis: ( abs ((e1 - e) . x) < r & abs ((e1 . x) - (e . x)) < r )

per cases ( x in dom e1 or not x in dom e1 ) ;

suppose A5: x in dom e1 ; :: thesis: ( abs ((e1 - e) . x) < r & abs ((e1 . x) - (e . x)) < r )

then A6: (e1 - e) . x = (e1 . x) - (e . x) by A3, A4, VALUED_1:13;
A7: ( e1 . x in REAL & e . x in REAL & r in REAL ) by XREAL_0:def 1;
dom e = dom (Intervals (e,r)) by Def3;
then A8: e1 . x in (Intervals (e,r)) . x by A5, A3, A2, CARD_3:18;
(Intervals (e,r)) . x = ].((e . x) - r),((e . x) + r).[ by A3, A5, Def3;
hence ( abs ((e1 - e) . x) < r & abs ((e1 . x) - (e . x)) < r ) by A6, A8, A7, FCONT_3:9; :: thesis: verum

end;

suppose A9: not x in dom e1 ; :: thesis: ( abs ((e1 - e) . x) < r & abs ((e1 . x) - (e . x)) < r )

then not x in dom (abs (e1 - e)) by A4, A3, VALUED_1:def 11;
then (abs (e1 - e)) . x = 0 by FUNCT_1:def 4;
then A10: abs ((e1 - e) . x) = 0 by VALUED_1:18;
( e1 . x = 0 & e . x = 0 ) by A3, A9, FUNCT_1:def 4;
hence ( abs ((e1 - e) . x) < r & abs ((e1 . x) - (e . x)) < r ) by A10, A1, A2; :: thesis: verum

end;

end;