let n be Nat; :: thesis: for p, q being Point of (TOP-REAL n)
for r being Real holds
( q in OpenHypercube (p,r) iff for i being Nat st i in Seg n holds
q . i in ].((p . i) - r),((p . i) + r).[ )
let p, q be Point of (TOP-REAL n); :: thesis: for r being Real holds
( q in OpenHypercube (p,r) iff for i being Nat st i in Seg n holds
q . i in ].((p . i) - r),((p . i) + r).[ )
let r be Real; :: thesis: ( q in OpenHypercube (p,r) iff for i being Nat st i in Seg n holds
q . i in ].((p . i) - r),((p . i) + r).[ )
A1: len q = n by CARD_1:def 7;
thus ( q in OpenHypercube (p,r) implies for i being Nat st i in Seg n holds
q . i in ].((p . i) - r),((p . i) + r).[ ) :: thesis: ( ( for i being Nat st i in Seg n holds
q . i in ].((p . i) - r),((p . i) + r).[ ) implies q in OpenHypercube (p,r) )

proof

assume A2: q in OpenHypercube (p,r) ; :: thesis: for i being Nat st i in Seg n holds
q . i in ].((p . i) - r),((p . i) + r).[
let i be Nat; :: thesis: ( i in Seg n implies q . i in ].((p . i) - r),((p . i) + r).[ )
assume A3: i in Seg n ; :: thesis: q . i in ].((p . i) - r),((p . i) + r).[
set P = PROJ (n,i);
dom (PROJ (n,i)) = the carrier of (TOP-REAL n) by FUNCT_2:def 1;
then A4: (PROJ (n,i)) . q in (PROJ (n,i)) .: (OpenHypercube (p,r)) by A2, FUNCT_1:def 6;
A5: (PROJ (n,i)) . q = q /. i by TOPREALC:def 6;
len q = n by CARD_1:def 7;
then dom q = Seg n by FINSEQ_1:def 3;
then q /. i = q . i by A3, PARTFUN1:def 6;
hence q . i in ].((p . i) - r),((p . i) + r).[ by A5, Th2, A3, A4; :: thesis: verum

end;

assume A6: for i being Nat st i in Seg n holds
q . i in ].((p . i) - r),((p . i) + r).[ ; :: thesis: q in OpenHypercube (p,r)
consider e being Point of (Euclid n) such that
A7: p = e and
A8: OpenHypercube (p,r) = OpenHypercube (e,r) by Def1;
set I = Intervals (e,r);
A9: dom (Intervals (e,r)) = dom e by EUCLID_9:def 3;
len p = n by CARD_1:def 7;
then A10: dom p = dom q by A1, FINSEQ_3:29;
A11: dom q = Seg n by A1, FINSEQ_1:def 3;

A12: now :: thesis: for x being object st x in dom q holds
q . x in (Intervals (e,r)) . x

let x be object ; :: thesis: ( x in dom q implies q . x in (Intervals (e,r)) . x )
assume A13: x in dom q ; :: thesis: q . x in (Intervals (e,r)) . x
then reconsider i = x as Nat ;
q . i in ].((p . i) - r),((p . i) + r).[ by A6, A13, A11;
hence q . x in (Intervals (e,r)) . x by EUCLID_9:def 3, A7, A13, A10; :: thesis: verum

end;

product (Intervals (e,r)) = OpenHypercube (p,r) by A8, EUCLID_9:def 4;
hence q in OpenHypercube (p,r) by A12, A7, A10, A9, CARD_3:9; :: thesis: verum