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 object such that
A3: x in Sphere (v,r) ;
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
x = w and
A4: ||.(v - w).|| = r by A3;
v - w <> 0. V by A2, A4, BHSP_1:26;
hence contradiction by A1, TARSKI:def 1; :: thesis: verum