let n be Nat; :: thesis: for r being Real
for a, o being Point of (Euclid 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 being Point of (Euclid 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 be Point of (Euclid n); :: thesis: ( a in Ball (o,r) implies for x being object holds
( |.((a - o) . x).| < r & |.((a . x) - (o . x)).| < r ) )
reconsider a1 = a, o1 = o as Point of (TOP-REAL n) by EUCLID:67;
A1: Ball (o,r) = Ball (o1,r) by TOPREAL9:13;
a - o = a1 - o1 ;
hence ( a in Ball (o,r) implies for x being object holds
( |.((a - o) . x).| < r & |.((a . x) - (o . x)).| < r ) ) by A1, Th9; :: thesis: verum