let X be RealNormSpace; for y1 being Point of X
for r being Real holds Ball (y1,r) = y1 + (Ball ((0. X),r))
let y1 be Point of X; for r being Real holds Ball (y1,r) = y1 + (Ball ((0. X),r))
let r be Real; Ball (y1,r) = y1 + (Ball ((0. X),r))
thus
Ball (y1,r) c= y1 + (Ball ((0. X),r))
XBOOLE_0:def 10 y1 + (Ball ((0. X),r)) c= Ball (y1,r)
let t be object ; TARSKI:def 3 ( not t in y1 + (Ball ((0. X),r)) or t in Ball (y1,r) )
assume
t in y1 + (Ball ((0. X),r))
; t in Ball (y1,r)
then consider z0 being Point of X such that
A3:
t = y1 + z0
and
A4:
z0 in Ball ((0. X),r)
;
set z1 = z0 + y1;
ex zz0 being Point of X st
( z0 = zz0 & ||.((0. X) - zz0).|| < r )
by A4;
then
||.(- z0).|| < r
by RLVECT_1:14;
then
||.z0.|| < r
by NORMSP_1:2;
then
||.(z0 + (0. X)).|| < r
by RLVECT_1:4;
then
||.(z0 + (y1 + (- y1))).|| < r
by RLVECT_1:5;
then
||.((z0 + y1) - y1).|| < r
by RLVECT_1:def 3;
then
||.(y1 - (z0 + y1)).|| < r
by NORMSP_1:7;
hence
t in Ball (y1,r)
by A3; verum