let n, i be Nat; :: thesis: for p, q being Point of (TOP-REAL n)
for r being Real
for R being real-valued FinSequence st i in Seg n & q in ClosedHypercube (p,R) & r in [.((p . i) - (R . i)),((p . i) + (R . i)).] holds
q +* (i,r) in ClosedHypercube (p,R)
let p, q be Point of (TOP-REAL n); :: thesis: for r being Real
for R being real-valued FinSequence st i in Seg n & q in ClosedHypercube (p,R) & r in [.((p . i) - (R . i)),((p . i) + (R . i)).] holds
q +* (i,r) in ClosedHypercube (p,R)
let r be Real; :: thesis: for R being real-valued FinSequence st i in Seg n & q in ClosedHypercube (p,R) & r in [.((p . i) - (R . i)),((p . i) + (R . i)).] holds
q +* (i,r) in ClosedHypercube (p,R)
let R be real-valued FinSequence; :: thesis: ( i in Seg n & q in ClosedHypercube (p,R) & r in [.((p . i) - (R . i)),((p . i) + (R . i)).] implies q +* (i,r) in ClosedHypercube (p,R) )
set H = ClosedHypercube (p,R);
set pr = q +* (i,r);
assume that
A1: i in Seg n and
A2: q in ClosedHypercube (p,R) and
A3: r in [.((p . i) - (R . i)),((p . i) + (R . i)).] ; :: thesis: q +* (i,r) in ClosedHypercube (p,R)
for j being Nat st j in Seg n holds
(q +* (i,r)) . j in [.((p . j) - (R . j)),((p . j) + (R . j)).]

proof

let j be Nat; :: thesis: ( j in Seg n implies (q +* (i,r)) . j in [.((p . j) - (R . j)),((p . j) + (R . j)).] )
assume A4: j in Seg n ; :: thesis: (q +* (i,r)) . j in [.((p . j) - (R . j)),((p . j) + (R . j)).]
A5: dom q = Seg (len q) by FINSEQ_1:def 3;
A6: len q = n by CARD_1:def 7;

per cases ( i <> j or i = j ) ;

suppose i <> j ; :: thesis: (q +* (i,r)) . j in [.((p . j) - (R . j)),((p . j) + (R . j)).]

then (q +* (i,r)) . j = q . j by FUNCT_7:32;
hence (q +* (i,r)) . j in [.((p . j) - (R . j)),((p . j) + (R . j)).] by Def2, A4, A2; :: thesis: verum

end;

suppose i = j ; :: thesis: (q +* (i,r)) . j in [.((p . j) - (R . j)),((p . j) + (R . j)).]

hence (q +* (i,r)) . j in [.((p . j) - (R . j)),((p . j) + (R . j)).] by FUNCT_7:31, A1, A5, A6, A3; :: thesis: verum

end;

end;

end;

hence q +* (i,r) in ClosedHypercube (p,R) by Def2; :: thesis: verum