let n, i be Nat; 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); 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; ( 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
; (PROJ (n,i)) .: (ClosedHypercube (p,R)) = [.((p . i) - (R . i)),((p . i) + (R . i)).]
hereby TARSKI:def 3,
XBOOLE_0:def 10 [.((p . i) - (R . i)),((p . i) + (R . i)).] c= (PROJ (n,i)) .: (ClosedHypercube (p,R))
let y be
object ;
( 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))
;
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;
verum
end;
let y be object ; TARSKI:def 3 ( 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)).]
; 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; verum