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
Sphere v,r is empty
let v be VECTOR of V; :: thesis: for r being Real st the carrier of V = {(0. V)} & r <> 0 holds
Sphere v,r is empty
let r be Real; :: thesis: ( the carrier of V = {(0. V)} & r <> 0 implies Sphere v,r is empty )
assume that
A1: the carrier of V = {(0. V)} and
A2: r <> 0 ; :: thesis: Sphere v,r is empty
assume not Sphere v,r is empty ; :: thesis: contradiction
then consider x being set such that
A3: x in Sphere v,r by XBOOLE_0:def 1;
Sphere v,r = { y where y is Point of V : ||.(v - y).|| = r } by BHSP_2:def 7;
then consider w being Point of V such that
A4: ( x = w & ||.(v - w).|| = r ) by A3;
v - w <> 0. V by A2, A4, BHSP_1:32;
hence contradiction by A1, TARSKI:def 1; :: thesis: verum