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 13;
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:116;
then (sqrt (Sum (sqr (a - o)))) ^2 = Sum (sqr (a - o)) by SQUARE_1:def 4;
then A4: Sum (sqr (a - o)) < r ^2 by A3, SQUARE_1:78;
A5: o - a = o - a by EUCLID:73;
A6: a - o = a - o by EUCLID:73;
then A7: sqr (a - o) = sqr (o - a) by A5, EUCLID:23;
A8: r > 0 by A2;
let x be set ; :: thesis: ( abs ((a - o) . x) < r & abs ((a . x) - (o . x)) < r )
A9: dom (a - o) = (dom a) /\ (dom o) by A6, VALUED_1:12;
A10: ( dom a = Seg n & dom o = Seg n ) by EUCLID:3;

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

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

then reconsider x = x as Nat ;
A12: (a - o) . x = (a . x) - (o . x) by A11, A6, A9, A10, VALUED_1:13;
A13: ( a /. x = a . x & o /. x = o . x ) by A11, A10, PARTFUN1:def 8;

now

assume (o . x) - (a . x) >= r ; :: thesis: contradiction
then A14: ((o . x) - (a . x)) ^2 >= r ^2 by A8, SQUARE_1:77;
Sum (sqr (o - a)) >= ((o /. x) - (a /. x)) ^2 by A11, A10, Th8;
hence contradiction by A4, A14, A7, A13, XXREAL_0:2; :: thesis: verum

end;

then A15: (o . x) - r < a . x by XREAL_1:13;

now

assume (a . x) - (o . x) >= r ; :: thesis: contradiction
then A16: ((a . x) - (o . x)) ^2 >= r ^2 by A8, SQUARE_1:77;
Sum (sqr (a - o)) >= ((a /. x) - (o /. x)) ^2 by A11, Th8;
hence contradiction by A4, A16, A13, XXREAL_0:2; :: thesis: verum

end;

then a . x < (o . x) + r by XREAL_1:21;
hence ( abs ((a - o) . x) < r & abs ((a . x) - (o . x)) < r ) by A12, A15, RINFSUP1:1; :: thesis: verum

end;

suppose A17: 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 A9, A10, VALUED_1:def 11;
then (abs (a - o)) . x = 0 by FUNCT_1:def 4;
then A18: abs ((a - o) . x) = 0 by VALUED_1:18;
( a . x = 0 & o . x = 0 ) by A10, A17, FUNCT_1:def 4;
hence ( abs ((a - o) . x) < r & abs ((a . x) - (o . x)) < r ) by A18, A2; :: thesis: verum

end;

end;