let n be Nat; :: thesis: for r being Real
for e, e1 being Point of (Euclid n) st ( n <> 0 or 0 < r ) & e1 in OpenHypercube (e,r) holds
for x being set holds
( |.((e1 - e) . x).| < r & |.((e1 . x) - (e . x)).| < r )
let r be Real; :: thesis: for e, e1 being Point of (Euclid n) st ( n <> 0 or 0 < r ) & e1 in OpenHypercube (e,r) holds
for x being set holds
( |.((e1 - e) . x).| < r & |.((e1 . x) - (e . x)).| < r )
let e, e1 be Point of (Euclid n); :: thesis: ( ( n <> 0 or 0 < r ) & e1 in OpenHypercube (e,r) implies for x being set holds
( |.((e1 - e) . x).| < r & |.((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
( |.((e1 - e) . x).| < r & |.((e1 . x) - (e . x)).| < r )
A3: ( dom e1 = Seg n & dom e = Seg n ) by FINSEQ_1:89;
A4: dom (e1 - e) = (dom e1) /\ (dom e) by VALUED_1:12;
let x be set ; :: thesis: ( |.((e1 - e) . x).| < r & |.((e1 . x) - (e . x)).| < r )

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

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

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

end;

suppose A8: not x in dom e1 ; :: thesis: ( |.((e1 - e) . x).| < r & |.((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 2;
then A9: |.((e1 - e) . x).| = 0 by VALUED_1:18;
( e1 . x = 0 & e . x = 0 ) by A3, A8, FUNCT_1:def 2;
hence ( |.((e1 - e) . x).| < r & |.((e1 . x) - (e . x)).| < r ) by A9, A1, A2; :: thesis: verum

end;

end;