let r be Real; :: thesis: for n being non zero Nat
for e being Point of (Euclid n) ex a being Element of REAL n st
( a = e & OpenHypercube (e,r) = OpenHyperInterval ((a - (n |-> r)),(a + (n |-> r))) )
let n be non zero Nat; :: thesis: for e being Point of (Euclid n) ex a being Element of REAL n st
( a = e & OpenHypercube (e,r) = OpenHyperInterval ((a - (n |-> r)),(a + (n |-> r))) )
let e be Point of (Euclid n); :: thesis: ex a being Element of REAL n st
( a = e & OpenHypercube (e,r) = OpenHyperInterval ((a - (n |-> r)),(a + (n |-> r))) )
reconsider a = e as Element of REAL n ;
reconsider p = e as Point of (TOP-REAL n) by EUCLID:67;
consider e0 being Point of (Euclid n) such that
A1: p = e0 and
A2: OpenHypercube (e0,r) = OpenHypercube (p,r) by TIETZE_2:def 1;
take a ; :: thesis: ( a = e & OpenHypercube (e,r) = OpenHyperInterval ((a - (n |-> r)),(a + (n |-> r))) )
thus a = e ; :: thesis: OpenHypercube (e,r) = OpenHyperInterval ((a - (n |-> r)),(a + (n |-> r)))
A3: OpenHypercube (e,r) c= OpenHyperInterval ((a - (n |-> r)),(a + (n |-> r)))

proof

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in OpenHypercube (e,r) or x in OpenHyperInterval ((a - (n |-> r)),(a + (n |-> r))) )
assume A4: x in OpenHypercube (e,r) ; :: thesis: x in OpenHyperInterval ((a - (n |-> r)),(a + (n |-> r)))
then reconsider y = x as Element of REAL n ;
for i being Nat st i in Seg n holds
y . i in ].((a - (n |-> r)) . i),((a + (n |-> r)) . i).[

proof

let i be Nat; :: thesis: ( i in Seg n implies y . i in ].((a - (n |-> r)) . i),((a + (n |-> r)) . i).[ )
assume A5: i in Seg n ; :: thesis: y . i in ].((a - (n |-> r)) . i),((a + (n |-> r)) . i).[
A6: (a - (n |-> r)) . i = (a . i) - ((n |-> r) . i) by RVSUM_1:27
.= (a . i) - r by A5, FINSEQ_2:57 ;
(a + (n |-> r)) . i = (a . i) + ((n |-> r) . i) by RVSUM_1:11
.= (a . i) + r by A5, FINSEQ_2:57 ;
hence y . i in ].((a - (n |-> r)) . i),((a + (n |-> r)) . i).[ by A5, A6, A1, A2, A4, TIETZE_2:4; :: thesis: verum

end;

hence x in OpenHyperInterval ((a - (n |-> r)),(a + (n |-> r))) by Def4; :: thesis: verum

end;

OpenHyperInterval ((a - (n |-> r)),(a + (n |-> r))) c= OpenHypercube (e,r)

proof

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in OpenHyperInterval ((a - (n |-> r)),(a + (n |-> r))) or x in OpenHypercube (e,r) )
assume A7: x in OpenHyperInterval ((a - (n |-> r)),(a + (n |-> r))) ; :: thesis: x in OpenHypercube (e,r)
then reconsider q = x as Element of (TOP-REAL n) by EUCLID:22;

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

let i be Nat; :: thesis: ( i in Seg n implies q . i in ].((p . i) - r),((p . i) + r).[ )
assume A8: i in Seg n ; :: thesis: q . i in ].((p . i) - r),((p . i) + r).[
consider y being Element of REAL n such that
A9: x = y and
A10: for i being Nat st i in Seg n holds
y . i in ].((a - (n |-> r)) . i),((a + (n |-> r)) . i).[ by A7, Def4;
A11: (a - (n |-> r)) . i = (a . i) - ((n |-> r) . i) by RVSUM_1:27
.= (a . i) - r by A8, FINSEQ_2:57 ;
(a + (n |-> r)) . i = (a . i) + ((n |-> r) . i) by RVSUM_1:11
.= (a . i) + r by A8, FINSEQ_2:57 ;
hence q . i in ].((p . i) - r),((p . i) + r).[ by A11, A8, A9, A10; :: thesis: verum

end;

hence x in OpenHypercube (e,r) by A1, A2, TIETZE_2:4; :: thesis: verum

end;

hence OpenHypercube (e,r) = OpenHyperInterval ((a - (n |-> r)),(a + (n |-> r))) by A3; :: thesis: verum