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

now :: thesis: for i being Nat st i in Seg n holds
p . i in [.((p . i) - (R . i)),((p . i) + (R . i)).]

let i be Nat; :: thesis: ( i in Seg n implies p . i in [.((p . i) - (R . i)),((p . i) + (R . i)).] )
assume A2: i in Seg n ; :: thesis: p . i in [.((p . i) - (R . i)),((p . i) + (R . i)).]

A3: now :: thesis: R . i >= 0

per cases ( i in dom R or not i in dom R ) ;

suppose i in dom R ; :: thesis: R . i >= 0

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

end;

suppose not i in dom R ; :: thesis: R . i >= 0

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

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: verum

end;

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