let n, i be Nat; :: thesis: for p being Point of (TOP-REAL n)
for R being real-valued FinSequence st i in Seg n & not ClosedHypercube (p,R) is empty holds
(PROJ (n,i)) .: (ClosedHypercube (p,R)) = [.((p . i) - (R . i)),((p . i) + (R . i)).]
let p be Point of (TOP-REAL n); :: thesis: for R being real-valued FinSequence st i in Seg n & not ClosedHypercube (p,R) is empty holds
(PROJ (n,i)) .: (ClosedHypercube (p,R)) = [.((p . i) - (R . i)),((p . i) + (R . i)).]
let R be real-valued FinSequence; :: thesis: ( i in Seg n & not ClosedHypercube (p,R) is empty implies (PROJ (n,i)) .: (ClosedHypercube (p,R)) = [.((p . i) - (R . i)),((p . i) + (R . i)).] )
set P = PROJ (n,i);
set H = ClosedHypercube (p,R);
set TR = TOP-REAL n;
assume that
A1: i in Seg n and
A2: not ClosedHypercube (p,R) is empty ; :: thesis: (PROJ (n,i)) .: (ClosedHypercube (p,R)) = [.((p . i) - (R . i)),((p . i) + (R . i)).]

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

let y be object ; :: thesis: ( y in (PROJ (n,i)) .: (ClosedHypercube (p,R)) implies y in [.((p . i) - (R . i)),((p . i) + (R . i)).] )
assume y in (PROJ (n,i)) .: (ClosedHypercube (p,R)) ; :: thesis: y in [.((p . i) - (R . i)),((p . i) + (R . i)).]
then consider x being object such that
A3: x in dom (PROJ (n,i)) and
A4: x in ClosedHypercube (p,R) and
A5: (PROJ (n,i)) . x = y by FUNCT_1:def 6;
reconsider x = x as Point of (TOP-REAL n) by A3;
len x = n by CARD_1:def 7;
then dom x = Seg n by FINSEQ_1:def 3;
then A6: x /. i = x . i by A1, PARTFUN1:def 6;
(PROJ (n,i)) . x = x /. i by TOPREALC:def 6;
hence y in [.((p . i) - (R . i)),((p . i) + (R . i)).] by A6, A1, A4, A5, Def2; :: thesis: verum

end;

let y be object ; :: according to TARSKI:def 3 :: thesis: ( not y in [.((p . i) - (R . i)),((p . i) + (R . i)).] or y in (PROJ (n,i)) .: (ClosedHypercube (p,R)) )
assume A7: y in [.((p . i) - (R . i)),((p . i) + (R . i)).] ; :: thesis: y in (PROJ (n,i)) .: (ClosedHypercube (p,R))
then reconsider r = y as Real ;
set pr = p +* (i,r);
A8: dom (PROJ (n,i)) = the carrier of (TOP-REAL n) by FUNCT_2:def 1;
A9: dom (p +* (i,r)) = Seg (len (p +* (i,r))) by FINSEQ_1:def 3;
len (p +* (i,r)) = n by CARD_1:def 7;
then A10: (p +* (i,r)) /. i = (p +* (i,r)) . i by A9, A1, PARTFUN1:def 6;
A11: dom p = Seg (len p) by FINSEQ_1:def 3;
for i being Nat st i in (Seg n) /\ (dom R) holds
R . i >= 0 by A2, Th4;
then p +* (i,r) in ClosedHypercube (p,R) by A1, Th6, A7, Th5;
then A12: (PROJ (n,i)) . (p +* (i,r)) in (PROJ (n,i)) .: (ClosedHypercube (p,R)) by A8, FUNCT_1:def 6;
A13: len p = n by CARD_1:def 7;
(PROJ (n,i)) . (p +* (i,r)) = (p +* (i,r)) /. i by TOPREALC:def 6;
hence y in (PROJ (n,i)) .: (ClosedHypercube (p,R)) by A13, A11, A10, A1, FUNCT_7:31, A12; :: thesis: verum