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

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