let X be RealNormSpace; :: thesis: 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; :: thesis: for r being Real holds Ball (y1,r) = y1 + (Ball ((0. X),r))

let r be Real; :: thesis: Ball (y1,r) = y1 + (Ball ((0. X),r))

thus Ball (y1,r) c= y1 + (Ball ((0. X),r)) :: according to XBOOLE_0:def 10 :: thesis: y1 + (Ball ((0. X),r)) c= Ball (y1,r)

assume t in y1 + (Ball ((0. X),r)) ; :: thesis: 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; :: thesis: verum

for r being Real holds Ball (y1,r) = y1 + (Ball ((0. X),r))

let y1 be Point of X; :: thesis: for r being Real holds Ball (y1,r) = y1 + (Ball ((0. X),r))

let r be Real; :: thesis: Ball (y1,r) = y1 + (Ball ((0. X),r))

thus Ball (y1,r) c= y1 + (Ball ((0. X),r)) :: according to XBOOLE_0:def 10 :: thesis: y1 + (Ball ((0. X),r)) c= Ball (y1,r)

proof

let t be object ; :: according to TARSKI:def 3 :: thesis: ( not t in y1 + (Ball ((0. X),r)) or t in Ball (y1,r) )
let t be object ; :: according to TARSKI:def 3 :: thesis: ( not t in Ball (y1,r) or t in y1 + (Ball ((0. X),r)) )

assume A1: t in Ball (y1,r) ; :: thesis: t in y1 + (Ball ((0. X),r))

then reconsider z1 = t as Point of X ;

set z0 = z1 - y1;

ex zz1 being Point of X st

( z1 = zz1 & ||.(y1 - zz1).|| < r ) by A1;

then ||.(- (z1 - y1)).|| < r by RLVECT_1:33;

then ||.((0. X) - (z1 - y1)).|| < r by RLVECT_1:14;

then A2: z1 - y1 in Ball ((0. X),r) ;

(z1 - y1) + y1 = z1 + ((- y1) + y1) by RLVECT_1:def 3;

then (z1 - y1) + y1 = z1 + (0. X) by RLVECT_1:5;

then z1 = (z1 - y1) + y1 by RLVECT_1:4;

hence t in y1 + (Ball ((0. X),r)) by A2; :: thesis: verum

end;assume A1: t in Ball (y1,r) ; :: thesis: t in y1 + (Ball ((0. X),r))

then reconsider z1 = t as Point of X ;

set z0 = z1 - y1;

ex zz1 being Point of X st

( z1 = zz1 & ||.(y1 - zz1).|| < r ) by A1;

then ||.(- (z1 - y1)).|| < r by RLVECT_1:33;

then ||.((0. X) - (z1 - y1)).|| < r by RLVECT_1:14;

then A2: z1 - y1 in Ball ((0. X),r) ;

(z1 - y1) + y1 = z1 + ((- y1) + y1) by RLVECT_1:def 3;

then (z1 - y1) + y1 = z1 + (0. X) by RLVECT_1:5;

then z1 = (z1 - y1) + y1 by RLVECT_1:4;

hence t in y1 + (Ball ((0. X),r)) by A2; :: thesis: verum

assume t in y1 + (Ball ((0. X),r)) ; :: thesis: 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; :: thesis: verum