let n be Nat; :: thesis: for r being Real
for a, o, p being Element of (TOP-REAL n) st a in Ball (o,r) holds
for x being object holds
( |.((a - o) . x).| < r & |.((a . x) - (o . x)).| < r )
let r be Real; :: thesis: for a, o, p being Element of (TOP-REAL n) st a in Ball (o,r) holds
for x being object holds
( |.((a - o) . x).| < r & |.((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 object holds
( |.((a - o) . x).| < r & |.((a . x) - (o . x)).| < r ) )
assume A1: a in Ball (o,r) ; :: thesis: for x being object holds
( |.((a - o) . x).| < r & |.((a . x) - (o . x)).| < r )
then A2: |.(a - o).| < r by 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 A3: Sum (sqr (a - o)) < r ^2 by A2, SQUARE_1:16;
A4: sqr (a - o) = sqr (o - a) by EUCLID:20;
A5: r > 0 by A1;
let x be object ; :: thesis: ( |.((a - o) . x).| < r & |.((a . x) - (o . x)).| < r )
A6: dom (a - o) = (dom a) /\ (dom o) by VALUED_1:12;
A7: ( 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 A8: x in dom a ; :: thesis: ( |.((a - o) . x).| < r & |.((a . x) - (o . x)).| < r )

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

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

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

end;

then A12: (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 A13: ((a . x) - (o . x)) ^2 >= r ^2 by A5, SQUARE_1:15;
Sum (sqr (a - o)) >= ((a /. x) - (o /. x)) ^2 by A8, Th8;
hence contradiction by A3, A13, A10, XXREAL_0:2; :: thesis: verum

end;

then a . x < (o . x) + r by XREAL_1:19;
hence ( |.((a - o) . x).| < r & |.((a . x) - (o . x)).| < r ) by A9, A12, RINFSUP1:1; :: thesis: verum

end;

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

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

end;

end;