let n, i be Nat; :: thesis: 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); :: thesis: 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; :: thesis: ( 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).[ ; :: thesis: 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 ; :: thesis: ( x in dom (Intervals (e,r)) implies (q +* (i,s)) . x in (Intervals (e,r)) . x )
assume A9: x in dom (Intervals (e,r)) ; :: thesis: (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; :: thesis: 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; :: thesis: verum