let n be Nat; 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; 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); ( ( 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)
; 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 ; ( |.((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
;
( |.((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;
verum end;