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
not 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
not Sphere (v,r) is empty
let r be Real; :: thesis: ( the carrier of V <> {(0. V)} & r > 0 implies not Sphere (v,r) is empty )
assume that
A1: the carrier of V <> {(0. V)} and
A2: r > 0 ; :: thesis: not Sphere (v,r) is empty

now :: thesis: not Sphere (v,r) is empty

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

suppose A3: v = 0. V ; :: thesis: not Sphere (v,r) is empty

ex u being VECTOR of V st u <> 0. V

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
A4: u in NonZero V by XBOOLE_0:def 1;
A5: not u in {(0. V)} by A4, XBOOLE_0:def 5;
reconsider u = u as VECTOR of V by A4;
take u ; :: thesis: u <> 0. V
thus u <> 0. V by A5, TARSKI:def 1; :: thesis: verum

end;

then consider u being VECTOR of V such that
A6: u <> 0. V ;
set a = ||.u.||;
A7: ||.u.|| <> 0 by A6, BHSP_1:26;
set u9 = (r * (1 / ||.u.||)) * u;
A8: ||.u.|| >= 0 by BHSP_1:28;
||.(v - ((r * (1 / ||.u.||)) * u)).|| = ||.(- ((r * (1 / ||.u.||)) * u)).|| by A3
.= ||.((r * (1 / ||.u.||)) * u).|| by BHSP_1:31
.= |.(r * (1 / ||.u.||)).| * ||.u.|| by BHSP_1:27 ;
then ||.(v - ((r * (1 / ||.u.||)) * u)).|| = (r * (1 / ||.u.||)) * ||.u.|| by A2, A8, ABSVALUE:def 1
.= r by A7, XCMPLX_1:109 ;
then (r * (1 / ||.u.||)) * u in { y where y is Point of V : ||.(v - y).|| = r } ;
hence not Sphere (v,r) is empty by BHSP_2:def 7; :: thesis: verum

end;

suppose A9: v <> 0. V ; :: thesis: not Sphere (v,r) is empty

set a = ||.v.||;
A10: ||.v.|| <> 0 by A9, BHSP_1:26;
set u9 = (1 - (r / ||.v.||)) * v;
A11: ||.(v - ((1 - (r / ||.v.||)) * v)).|| = ||.((1 * v) - ((1 - (r / ||.v.||)) * v)).|| by RLVECT_1:def 8
.= ||.((1 - (1 - (r / ||.v.||))) * v).|| by RLVECT_1:35
.= |.(r / ||.v.||).| * ||.v.|| by BHSP_1:27 ;
||.v.|| >= 0 by BHSP_1:28;
then ||.(v - ((1 - (r / ||.v.||)) * v)).|| = (r / ||.v.||) * ||.v.|| by A2, A11, ABSVALUE:def 1
.= r / (||.v.|| / ||.v.||) by XCMPLX_1:81
.= r by A10, XCMPLX_1:51 ;
then (1 - (r / ||.v.||)) * v in { y where y is Point of V : ||.(v - y).|| = r } ;
hence not Sphere (v,r) is empty by BHSP_2:def 7; :: thesis: verum

end;

end;

end;

hence not Sphere (v,r) is empty ; :: thesis: verum