let V be RealUnitarySpace; :: thesis: for v being VECTOR of V
for r being Real st the carrier of V <> {(0. V)} & r > 0 holds
ex w being VECTOR of V st
( w <> v & w in Ball (v,r) )
let v be VECTOR of V; :: thesis: for r being Real st the carrier of V <> {(0. V)} & r > 0 holds
ex w being VECTOR of V st
( w <> v & w in Ball (v,r) )
let r be Real; :: thesis: ( the carrier of V <> {(0. V)} & r > 0 implies ex w being VECTOR of V st
( w <> v & w in Ball (v,r) ) )
assume that
A1: the carrier of V <> {(0. V)} and
A2: r > 0 ; :: thesis: ex w being VECTOR of V st
( w <> v & w in Ball (v,r) )
consider r9 being Real such that
A3: 0 < r9 and
A4: r9 < r by A2, XREAL_1:5;
reconsider r9 = r9 as Real ;

now :: thesis: ex w being VECTOR of V st
( w <> v & w in Ball (v,r) )

per cases ( v = 0. V or v <> 0. V ) ;

suppose A5: v = 0. V ; :: thesis: ex w being VECTOR of V st
( w <> v & w in Ball (v,r) )

ex w being VECTOR of V st
( w <> 0. V & ||.w.|| < r )

proof

not the carrier of V c= {(0. V)} by A1;
then NonZero V <> {} by XBOOLE_1:37;
then consider u being object such that
A6: u in NonZero V by XBOOLE_0:def 1;
A7: not u in {(0. V)} by A6, XBOOLE_0:def 5;
reconsider u = u as VECTOR of V by A6;
A8: u <> 0. V by A7, TARSKI:def 1;
then A9: ||.u.|| <> 0 by BHSP_1:26;
set a = ||.u.||;
A10: ||.u.|| >= 0 by BHSP_1:28;
take w = (r9 / ||.u.||) * u; :: thesis: ( w <> 0. V & ||.w.|| < r )
A11: ||.w.|| = |.(r9 / ||.u.||).| * ||.u.|| by BHSP_1:27
.= (r9 / ||.u.||) * ||.u.|| by A3, A10, ABSVALUE:def 1
.= r9 / (||.u.|| / ||.u.||) by XCMPLX_1:81
.= r9 by A9, XCMPLX_1:51 ;
r9 / ||.u.|| > 0 by A3, A9, A10, XREAL_1:139;
hence ( w <> 0. V & ||.w.|| < r ) by A4, A8, A11, RLVECT_1:11; :: thesis: verum

end;

then consider u being VECTOR of V such that
A12: u <> 0. V and
A13: ||.u.|| < r ;
||.(v - u).|| = ||.(- u).|| by A5
.= ||.u.|| by BHSP_1:31 ;
then u in { y where y is Point of V : ||.(v - y).|| < r } by A13;
then u in Ball (v,r) by BHSP_2:def 5;
hence ex w being VECTOR of V st
( w <> v & w in Ball (v,r) ) by A5, A12; :: thesis: verum

end;

suppose A14: v <> 0. V ; :: thesis: ex w being VECTOR of V st
( w <> v & w in Ball (v,r) )

set a = ||.v.||;
A15: ||.v.|| <> 0 by A14, BHSP_1:26;
set u9 = (1 - (r9 / ||.v.||)) * v;
A16: ||.(v - ((1 - (r9 / ||.v.||)) * v)).|| = ||.((1 * v) - ((1 - (r9 / ||.v.||)) * v)).|| by RLVECT_1:def 8
.= ||.((1 - (1 - (r9 / ||.v.||))) * v).|| by RLVECT_1:35
.= |.(r9 / ||.v.||).| * ||.v.|| by BHSP_1:27 ;
||.v.|| >= 0 by BHSP_1:28;
then A17: ||.(v - ((1 - (r9 / ||.v.||)) * v)).|| = (r9 / ||.v.||) * ||.v.|| by A3, A16, ABSVALUE:def 1
.= r9 / (||.v.|| / ||.v.||) by XCMPLX_1:81
.= r9 by A15, XCMPLX_1:51 ;
then v - ((1 - (r9 / ||.v.||)) * v) <> 0. V by A3, BHSP_1:26;
then A18: v <> (1 - (r9 / ||.v.||)) * v by RLVECT_1:15;
(1 - (r9 / ||.v.||)) * v in { y where y is Point of V : ||.(v - y).|| < r } by A4, A17;
then (1 - (r9 / ||.v.||)) * v in Ball (v,r) by BHSP_2:def 5;
hence ex w being VECTOR of V st
( w <> v & w in Ball (v,r) ) by A18; :: thesis: verum

end;

end;

end;

hence ex w being VECTOR of V st
( w <> v & w in Ball (v,r) ) ; :: thesis: verum