for n, i being 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)