let r be Real; :: thesis: for n being non zero Nat
for p being Element of (EMINFTY n)
for e being Point of (Euclid n) st e = p holds
Ball (p,r) = OpenHypercube (e,r)
let n be non zero Nat; :: thesis: for p being Element of (EMINFTY n)
for e being Point of (Euclid n) st e = p holds
Ball (p,r) = OpenHypercube (e,r)
let p be Element of (EMINFTY n); :: thesis: for e being Point of (Euclid n) st e = p holds
Ball (p,r) = OpenHypercube (e,r)
let e be Point of (Euclid n); :: thesis: ( e = p implies Ball (p,r) = OpenHypercube (e,r) )
assume A1: e = p ; :: thesis: Ball (p,r) = OpenHypercube (e,r)
Ball (p,r) = product (Intervals ((@ p),r)) by Th68;
hence Ball (p,r) = OpenHypercube (e,r) by A1; :: thesis: verum