let n, i be Nat; for p, q being Point of (TOP-REAL n)
for r, s being Real st q in OpenHypercube (p,r) & s in ].((p . i) - r),((p . i) + r).[ holds
q +* (i,s) in OpenHypercube (p,r)
let p, q be Point of (TOP-REAL n); for r, s being Real st q in OpenHypercube (p,r) & s in ].((p . i) - r),((p . i) + r).[ holds
q +* (i,s) in OpenHypercube (p,r)
let r, s be Real; ( q in OpenHypercube (p,r) & s in ].((p . i) - r),((p . i) + r).[ implies q +* (i,s) in OpenHypercube (p,r) )
assume that
A1:
q in OpenHypercube (p,r)
and
A2:
s in ].((p . i) - r),((p . i) + r).[
; q +* (i,s) in OpenHypercube (p,r)
consider e being Point of (Euclid n) such that
A3:
p = e
and
A4:
OpenHypercube (p,r) = OpenHypercube (e,r)
by Def1;
set OH = OpenHypercube (e,r);
set I = Intervals (e,r);
set qs = q +* (i,s);
A5:
OpenHypercube (e,r) = product (Intervals (e,r))
by EUCLID_9:def 4;
then A6:
dom q = dom (Intervals (e,r))
by A4, A1, CARD_3:9;
A7:
dom (Intervals (e,r)) = dom e
by EUCLID_9:def 3;
A8:
for x being object st x in dom (Intervals (e,r)) holds
(q +* (i,s)) . x in (Intervals (e,r)) . x
proof
let x be
object ;
( x in dom (Intervals (e,r)) implies (q +* (i,s)) . x in (Intervals (e,r)) . x )
assume A9:
x in dom (Intervals (e,r))
;
(q +* (i,s)) . x in (Intervals (e,r)) . x
then A10:
(Intervals (e,r)) . x = ].((e . x) - r),((e . x) + r).[
by A7, EUCLID_9:def 3;
A11:
q . x in (Intervals (e,r)) . x
by A9, A1, A5, A4, CARD_3:9;
(
i = x or
i <> x )
;
hence
(q +* (i,s)) . x in (Intervals (e,r)) . x
by A6, A9, A3, FUNCT_7:31, FUNCT_7:32, A2, A10, A11;
verum
end;
dom (q +* (i,s)) = dom q
by FUNCT_7:30;
hence
q +* (i,s) in OpenHypercube (p,r)
by A4, A8, CARD_3:9, A6, A5; verum