let n, i be Nat; :: thesis: for p being Point of (TOP-REAL n)
for r being Real st i in Seg n holds
(PROJ (n,i)) .: (OpenHypercube (p,r)) = ].((p . i) - r),((p . i) + r).[
let p be Point of (TOP-REAL n); :: thesis: for r being Real st i in Seg n holds
(PROJ (n,i)) .: (OpenHypercube (p,r)) = ].((p . i) - r),((p . i) + r).[
let r be Real; :: thesis: ( i in Seg n implies (PROJ (n,i)) .: (OpenHypercube (p,r)) = ].((p . i) - r),((p . i) + r).[ )
assume A1: i in Seg n ; :: thesis: (PROJ (n,i)) .: (OpenHypercube (p,r)) = ].((p . i) - r),((p . i) + r).[
consider e being Point of (Euclid n) such that
A2: p = e and
A3: OpenHypercube (p,r) = OpenHypercube (e,r) by Def1;
set OH = OpenHypercube (e,r);
set I = Intervals (e,r);
A4: OpenHypercube (e,r) = product (Intervals (e,r)) by EUCLID_9:def 4;
len e = n by CARD_1:def 7;
then A5: dom e = Seg n by FINSEQ_1:def 3;
then A6: (Intervals (e,r)) . i = ].((e . i) - r),((e . i) + r).[ by A1, EUCLID_9:def 3;

hereby :: according to TARSKI:def 3,XBOOLE_0:def 10 :: thesis: ].((p . i) - r),((p . i) + r).[ c= (PROJ (n,i)) .: (OpenHypercube (p,r))

let y be object ; :: thesis: ( y in (PROJ (n,i)) .: (OpenHypercube (p,r)) implies y in ].((p . i) - r),((p . i) + r).[ )
assume y in (PROJ (n,i)) .: (OpenHypercube (p,r)) ; :: thesis: y in ].((p . i) - r),((p . i) + r).[
then consider x being object such that
A7: x in dom (PROJ (n,i)) and
A8: x in OpenHypercube (e,r) and
A9: (PROJ (n,i)) . x = y by A3, FUNCT_1:def 6;
reconsider x = x as Point of (TOP-REAL n) by A7;
A10: dom (Intervals (e,r)) = dom x by A8, A4, CARD_3:9;
then A11: dom x = Seg n by EUCLID_9:def 3, A5;
then A12: x /. i = x . i by A1, PARTFUN1:def 6;
x . i in (Intervals (e,r)) . i by A11, A10, CARD_3:9, A8, A4, A1;
hence y in ].((p . i) - r),((p . i) + r).[ by A2, TOPREALC:def 6, A12, A6, A9; :: thesis: verum

end;

let y be object ; :: according to TARSKI:def 3 :: thesis: ( not y in ].((p . i) - r),((p . i) + r).[ or y in (PROJ (n,i)) .: (OpenHypercube (p,r)) )
assume A13: y in ].((p . i) - r),((p . i) + r).[ ; :: thesis: y in (PROJ (n,i)) .: (OpenHypercube (p,r))
then reconsider s = y as Real ;
A14: s < (e . i) + r by A2, A13, XXREAL_1:4;
set ps = p +* (i,s);
(e . i) - r < s by A2, A13, XXREAL_1:4;
then (e . i) + (- r) < (e . i) + r by A14, XXREAL_0:2;
then r > 0 by XREAL_1:6;
then A15: p +* (i,s) in OpenHypercube (e,r) by A2, A3, EUCLID_9:11, Th1, A13;
len (p +* (i,s)) = n by CARD_1:def 7;
then A16: dom (p +* (i,s)) = Seg n by FINSEQ_1:def 3;
len p = n by CARD_1:def 7;
then A17: dom p = Seg n by FINSEQ_1:def 3;
A18: dom (PROJ (n,i)) = the carrier of (TOP-REAL n) by FUNCT_2:def 1;
(PROJ (n,i)) . (p +* (i,s)) = (p +* (i,s)) /. i by TOPREALC:def 6
.= (p +* (i,s)) . i by A16, A1, PARTFUN1:def 6
.= s by A17, A1, FUNCT_7:31 ;
hence y in (PROJ (n,i)) .: (OpenHypercube (p,r)) by A3, A18, A15, FUNCT_1:def 6; :: thesis: verum