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)
proof
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;
let t be object ; :: according to TARSKI:def 3 :: thesis: ( not t in y1 + (Ball ((0. X),r)) or t in 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