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

(abs (a - o)) . j <= (n |-> r) . j ;

ex j being Nat st

( j in Seg n & (abs (a - o)) . j < (n |-> r) . j )

|.(Sum (a - o)).| <= Sum (abs (a - o)) by Th21;

hence |.(Sum (a - o)).| < n * r by A3, A8, XXREAL_0:2; :: thesis: verum

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

then A7:
for j being Nat st j in Seg n holds
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;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

(abs (a - o)) . j <= (n |-> r) . j ;

ex j being Nat st

( j in Seg n & (abs (a - o)) . j < (n |-> r) . j )

proof

then A8:
Sum (abs (a - o)) < Sum (n |-> r)
by A7, RVSUM_1:83;
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;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

|.(Sum (a - o)).| <= Sum (abs (a - o)) by Th21;

hence |.(Sum (a - o)).| < n * r by A3, A8, XXREAL_0:2; :: thesis: verum