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
Ball v,r = {(0. V)}
let v be VECTOR of V; :: thesis: for r being Real st the carrier of V = {(0. V)} & r > 0 holds
Ball v,r = {(0. V)}
let r be Real; :: thesis: ( the carrier of V = {(0. V)} & r > 0 implies Ball v,r = {(0. V)} )
assume that
A1: the carrier of V = {(0. V)} and
A2: r > 0 ; :: thesis: Ball v,r = {(0. V)}
for w being VECTOR of V st w in {(0. V)} holds
w in Ball v,r

proof

let w be VECTOR of V; :: thesis: ( w in {(0. V)} implies w in Ball v,r )
assume A3: w in {(0. V)} ; :: thesis: w in Ball v,r
v = 0. V by A1, TARSKI:def 1;
then ||.(v - w).|| = ||.((0. V) - (0. V)).|| by A3, TARSKI:def 1
.= ||.(0. V).|| by RLVECT_1:26
.= 0 by BHSP_1:32 ;
then w in { y where y is Point of V : ||.(v - y).|| < r } by A2;
hence w in Ball v,r by BHSP_2:def 5; :: thesis: verum

end;

then {(0. V)} c= Ball v,r by SUBSET_1:7;
hence Ball v,r = {(0. V)} by A1, XBOOLE_0:def 10; :: thesis: verum