let X be RealNormSpace; :: thesis: for r, a being Real st 0 < a holds
Ball ((0. X),(a * r)) = a * (Ball ((0. X),r))
let r, a be Real; :: thesis: ( 0 < a implies Ball ((0. X),(a * r)) = a * (Ball ((0. X),r)) )
assume A1: 0 < a ; :: thesis: Ball ((0. X),(a * r)) = a * (Ball ((0. X),r))
thus Ball ((0. X),(a * r)) c= a * (Ball ((0. X),r)) :: according to XBOOLE_0:def 10 :: thesis: a * (Ball ((0. X),r)) c= Ball ((0. X),(a * r))

proof

let z be object ; :: according to TARSKI:def 3 :: thesis: ( not z in Ball ((0. X),(a * r)) or z in a * (Ball ((0. X),r)) )
assume A2: z in Ball ((0. X),(a * r)) ; :: thesis: z in a * (Ball ((0. X),r))
then reconsider z1 = z as Point of X ;
ex zz1 being Point of X st
( z1 = zz1 & ||.((0. X) - zz1).|| < a * r ) by A2;
then ||.(- z1).|| < a * r by RLVECT_1:14;
then ||.z1.|| < a * r by NORMSP_1:2;
then (a ") * ||.z1.|| < (a ") * (a * r) by A1, XREAL_1:68;
then (a ") * ||.z1.|| < (a * (a ")) * r ;
then A3: (a ") * ||.z1.|| < 1 * r by A1, XCMPLX_0:def 7;
set y1 = (a ") * z1;
||.((a ") * z1).|| = |.(a ").| * ||.z1.|| by NORMSP_1:def 1
.= (a ") * ||.z1.|| by A1, ABSVALUE:def 1 ;
then ||.(- ((a ") * z1)).|| < r by A3, NORMSP_1:2;
then ||.((0. X) - ((a ") * z1)).|| < r by RLVECT_1:14;
then A4: (a ") * z1 in Ball ((0. X),r) ;
a * ((a ") * z1) = (a * (a ")) * z1 by RLVECT_1:def 7
.= 1 * z1 by A1, XCMPLX_0:def 7
.= z1 by RLVECT_1:def 8 ;
hence z in a * (Ball ((0. X),r)) by A4; :: thesis: verum

end;

let z be object ; :: according to TARSKI:def 3 :: thesis: ( not z in a * (Ball ((0. X),r)) or z in Ball ((0. X),(a * r)) )
assume A5: z in a * (Ball ((0. X),r)) ; :: thesis: z in Ball ((0. X),(a * r))
then reconsider z1 = z as Point of X ;
consider y1 being Point of X such that
A6: z1 = a * y1 and
A7: y1 in Ball ((0. X),r) by A5;
ex yy1 being Point of X st
( y1 = yy1 & ||.((0. X) - yy1).|| < r ) by A7;
then ||.(- y1).|| < r by RLVECT_1:14;
then A8: ||.y1.|| < r by NORMSP_1:2;
||.z1.|| = |.a.| * ||.y1.|| by A6, NORMSP_1:def 1
.= a * ||.y1.|| by A1, ABSVALUE:def 1 ;
then ||.z1.|| < a * r by A1, A8, XREAL_1:68;
then ||.(- z1).|| < a * r by NORMSP_1:2;
then ||.((0. X) - z1).|| < a * r by RLVECT_1:14;
hence z in Ball ((0. X),(a * r)) ; :: thesis: verum