let n be Nat; :: thesis: for r being Real
for a, o being Point of (TOP-REAL n) st n <> 0 & a in Ball (o,r) holds
|.(Sum (a - o)).| < n * r
let r be Real; :: thesis: for a, o being Point of (TOP-REAL n) st n <> 0 & a in Ball (o,r) holds
|.(Sum (a - o)).| < n * r
let a, o be Point of (TOP-REAL n); :: thesis: ( n <> 0 & a in Ball (o,r) implies |.(Sum (a - o)).| < n * r )
set R1 = a - o;
set R2 = n |-> r;
assume that
A1: n <> 0 and
A2: a in Ball (o,r) ; :: thesis: |.(Sum (a - o)).| < n * r
A3: Sum (n |-> r) = n * r by RVSUM_1:80;
A5: for j being Nat st j in Seg n holds
(abs (a - o)) . j < (n |-> r) . j
proof
let j be Nat; :: thesis: ( j in Seg n implies (abs (a - o)) . j < (n |-> r) . j )
assume j in Seg n ; :: thesis: (abs (a - o)) . j < (n |-> r) . j
then A6: (n |-> r) . j = r by FINSEQ_2:57;
|.((a - o) . j).| < r by A2, EUCLID_9:9;
hence (abs (a - o)) . j < (n |-> r) . j by A6, VALUED_1:18; :: thesis: verum
end;
then A7: for j being Nat st j in Seg n holds
(abs (a - o)) . j <= (n |-> r) . j ;
ex j being Nat st
( j in Seg n & (abs (a - o)) . j < (n |-> r) . j )
proof
take 1 ; :: thesis: ( 1 in Seg n & (abs (a - o)) . 1 < (n |-> r) . 1 )
1 <= n by A1, NAT_1:14;
hence 1 in Seg n ; :: thesis: (abs (a - o)) . 1 < (n |-> r) . 1
hence (abs (a - o)) . 1 < (n |-> r) . 1 by A5; :: thesis: verum
end;
then A8: Sum (abs (a - o)) < Sum (n |-> r) by A7, RVSUM_1:83;
|.(Sum (a - o)).| <= Sum (abs (a - o)) by Th21;
hence |.(Sum (a - o)).| < n * r by A3, A8, XXREAL_0:2; :: thesis: verum