let n be Nat; :: thesis: for r being real number
for e1, e being Point of (Euclid n) st n <> 0 & e1 in OpenHypercube (e,r) holds
Sum (sqr (e1 - e)) < n * (r ^2)
let r be real number ; :: thesis: for e1, e being Point of (Euclid n) st n <> 0 & e1 in OpenHypercube (e,r) holds
Sum (sqr (e1 - e)) < n * (r ^2)
let e1, e be Point of (Euclid n); :: thesis: ( n <> 0 & e1 in OpenHypercube (e,r) implies Sum (sqr (e1 - e)) < n * (r ^2) )
assume that
A1: n <> 0 and
A2: e1 in OpenHypercube (e,r) ; :: thesis: Sum (sqr (e1 - e)) < n * (r ^2)
set R1 = sqr (e1 - e);
set R2 = n |-> (r ^2);
A3: REAL n = n -tuples_on REAL ;
A4: sqr (e1 - e) in n -tuples_on REAL by Th2;
A5: n |-> (r ^2) in n -tuples_on REAL by A3, Th2;

A6: now

let i be Nat; :: thesis: ( i in Seg n implies (sqr (e1 - e)) . i < (n |-> (r ^2)) . i )
assume A7: i in Seg n ; :: thesis: (sqr (e1 - e)) . i < (n |-> (r ^2)) . i
A8: ( dom e1 = Seg n & dom e = Seg n ) by FINSEQ_1:89;
dom (e1 - e) = (dom e1) /\ (dom e) by VALUED_1:12;
then A9: (e1 - e) . i = (e1 . i) - (e . i) by A7, A8, VALUED_1:13;
A10: (sqr (e1 - e)) . i = ((e1 - e) . i) ^2 by VALUED_1:11;
A11: (n |-> (r ^2)) . i = r ^2 by A7, FINSEQ_2:57;
A12: abs ((e1 . i) - (e . i)) < r by A1, A2, Th14;
((e1 - e) . i) ^2 = (abs ((e1 - e) . i)) ^2 by COMPLEX1:75;
hence (sqr (e1 - e)) . i < (n |-> (r ^2)) . i by A9, A10, A11, A12, SQUARE_1:16; :: thesis: verum

end;

then A13: for i being Nat st i in Seg n holds
(sqr (e1 - e)) . i <= (n |-> (r ^2)) . i ;
ex i being Nat st
( i in Seg n & (sqr (e1 - e)) . i < (n |-> (r ^2)) . i )

proof

consider i being set such that
A14: i in Seg n by A1, XBOOLE_0:def 1;
reconsider i = i as Nat by A14;
take i ; :: thesis: ( i in Seg n & (sqr (e1 - e)) . i < (n |-> (r ^2)) . i )
thus ( i in Seg n & (sqr (e1 - e)) . i < (n |-> (r ^2)) . i ) by A14, A6; :: thesis: verum

end;

then Sum (sqr (e1 - e)) < Sum (n |-> (r ^2)) by A4, A5, A13, RVSUM_1:83;
hence Sum (sqr (e1 - e)) < n * (r ^2) by RVSUM_1:80; :: thesis: verum