let n be Nat; :: thesis: for r being real number
for a, o, p being Element of (TOP-REAL n) st a in Ball (o,r) holds
for x being set holds
( abs ((a - o) . x) < r & abs ((a . x) - (o . x)) < r )
let r be real number ; :: thesis: for a, o, p being Element of (TOP-REAL n) st a in Ball (o,r) holds
for x being set holds
( abs ((a - o) . x) < r & abs ((a . x) - (o . x)) < r )
let a, o, p be Element of (TOP-REAL n); :: thesis: ( a in Ball (o,r) implies for x being set holds
( abs ((a - o) . x) < r & abs ((a . x) - (o . x)) < r ) )
A1: n in NAT by ORDINAL1:def 12;
assume A2: a in Ball (o,r) ; :: thesis: for x being set holds
( abs ((a - o) . x) < r & abs ((a . x) - (o . x)) < r )
then A3: |.(a - o).| < r by A1, TOPREAL9:7;
0 <= Sum (sqr (a - o)) by RVSUM_1:86;
then (sqrt (Sum (sqr (a - o)))) ^2 = Sum (sqr (a - o)) by SQUARE_1:def 2;
then A4: Sum (sqr (a - o)) < r ^2 by A3, SQUARE_1:16;
A5: sqr (a - o) = sqr (o - a) by EUCLID:20;
A6: r > 0 by A2;
let x be set ; :: thesis: ( abs ((a - o) . x) < r & abs ((a . x) - (o . x)) < r )
A7: dom (a - o) = (dom a) /\ (dom o) by VALUED_1:12;
A8: ( dom a = Seg n & dom o = Seg n ) by FINSEQ_1:89;

per cases ( x in dom a or not x in dom a ) ;

suppose A9: x in dom a ; :: thesis: ( abs ((a - o) . x) < r & abs ((a . x) - (o . x)) < r )

then reconsider x = x as Nat ;
A10: (a - o) . x = (a . x) - (o . x) by A9, A7, A8, VALUED_1:13;
A11: ( a /. x = a . x & o /. x = o . x ) by A9, A8, PARTFUN1:def 6;

now :: thesis: not (o . x) - (a . x) >= r

assume (o . x) - (a . x) >= r ; :: thesis: contradiction
then A12: ((o . x) - (a . x)) ^2 >= r ^2 by A6, SQUARE_1:15;
Sum (sqr (o - a)) >= ((o /. x) - (a /. x)) ^2 by A9, A8, Th8;
hence contradiction by A4, A12, A5, A11, XXREAL_0:2; :: thesis: verum

end;

then A13: (o . x) - r < a . x by XREAL_1:11;

now :: thesis: not (a . x) - (o . x) >= r

assume (a . x) - (o . x) >= r ; :: thesis: contradiction
then A14: ((a . x) - (o . x)) ^2 >= r ^2 by A6, SQUARE_1:15;
Sum (sqr (a - o)) >= ((a /. x) - (o /. x)) ^2 by A9, Th8;
hence contradiction by A4, A14, A11, XXREAL_0:2; :: thesis: verum

end;

then a . x < (o . x) + r by XREAL_1:19;
hence ( abs ((a - o) . x) < r & abs ((a . x) - (o . x)) < r ) by A10, A13, RINFSUP1:1; :: thesis: verum

end;

suppose A15: not x in dom a ; :: thesis: ( abs ((a - o) . x) < r & abs ((a . x) - (o . x)) < r )

then not x in dom (abs (a - o)) by A7, A8, VALUED_1:def 11;
then (abs (a - o)) . x = 0 by FUNCT_1:def 2;
then A16: abs ((a - o) . x) = 0 by VALUED_1:18;
( a . x = 0 & o . x = 0 ) by A8, A15, FUNCT_1:def 2;
hence ( abs ((a - o) . x) < r & abs ((a . x) - (o . x)) < r ) by A16, A2; :: thesis: verum

end;

end;