let n be Nat; :: thesis: for r being Real

for e being Point of (Euclid n) st n <> 0 holds

OpenHypercube (e,r) c= Ball (e,(r * (sqrt n)))

let r be Real; :: 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:87;

hence OpenHypercube (e,r) c= Ball (e,(r * (sqrt n))) by A2, XCMPLX_1:74; :: thesis: verum

for e being Point of (Euclid n) st n <> 0 holds

OpenHypercube (e,r) c= Ball (e,(r * (sqrt n)))

let r be Real; :: 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:87;

hence OpenHypercube (e,r) c= Ball (e,(r * (sqrt n))) by A2, XCMPLX_1:74; :: thesis: verum