let n be Nat; :: thesis: for r being real number
for e being Point of (Euclid n) st n <> 0 holds
OpenHypercube e,r c= Ball e,(r * (sqrt n))
let r be real number ; :: thesis: for e being Point of (Euclid n) st n <> 0 holds
OpenHypercube e,r c= Ball e,(r * (sqrt n))
let e be Point of (Euclid n); :: thesis: ( n <> 0 implies OpenHypercube e,r c= Ball e,(r * (sqrt n)) )
assume A1: n <> 0 ; :: thesis: OpenHypercube e,r c= Ball e,(r * (sqrt n))
then A2: OpenHypercube e,((r * (sqrt n)) / (sqrt n)) c= Ball e,(r * (sqrt n)) by Th17;
(r / (sqrt n)) * (sqrt n) = r by A1, XCMPLX_1:88;
hence OpenHypercube e,r c= Ball e,(r * (sqrt n)) by A2, XCMPLX_1:75; :: thesis: verum