let n be Nat; :: thesis:
let p be Point of (TOP-REAL n); :: thesis:
let R be real-valued FinSequence; :: thesis:
assume A1: for i being Nat st i in (Seg n) /\ (dom R) holds
R . i >= 0 ; :: thesis:

let i be Nat; :: thesis:
assume A2: i in Seg n ; :: thesis:

A3: now :: thesis:

suppose i in dom R ; :: thesis:

then i in (Seg n) /\ (dom R) by A2, XBOOLE_0:def 4;
hence R . i >= 0 by A1; :: thesis:

end;

suppose not i in dom R ; :: thesis:

hence R . i >= 0 by FUNCT_1:def 2; :: thesis:

end;

end;

end;

then A4: (p . i) + (R . i) >= p . i by XREAL_1:40;
(p . i) - (R . i) <= p . i by A3, XREAL_1:43;
hence p . i in [.((p . i) - (R . i)),((p . i) + (R . i)).] by A4, XXREAL_1:1; :: thesis:

end;

hence p in ClosedHypercube (p,R) by Def2; :: thesis: