let X be RealNormSpace; :: thesis: for r being real number
for a being Real st 0 < a holds
Ball (0. X),(a * r) = a * (Ball (0. X),r)
let r be real number ; :: thesis: for a being Real st 0 < a holds
Ball (0. X),(a * r) = a * (Ball (0. X),r)
let 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 set ; :: 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:27;
then ||.z1.|| < a * r by NORMSP_1:6;
then (a " ) * ||.z1.|| < (a " ) * (a * r) by A1, XREAL_1:70;
then (a " ) * ||.z1.|| < (a * (a " )) * r ;
then A3: (a " ) * ||.z1.|| < 1 * r by A1, XCMPLX_0:def 7;
set y1 = (a " ) * z1;
||.((a " ) * z1).|| = (abs (a " )) * ||.z1.|| by NORMSP_1:def 2
.= (a " ) * ||.z1.|| by A1, ABSVALUE:def 1 ;
then ||.(- ((a " ) * z1)).|| < r by A3, NORMSP_1:6;
then ||.((0. X) - ((a " ) * z1)).|| < r by RLVECT_1:27;
then A4: (a " ) * z1 in Ball (0. X),r ;
a * ((a " ) * z1) = (a * (a " )) * z1 by RLVECT_1:def 9
.= 1 * z1 by A1, XCMPLX_0:def 7
.= z1 by RLVECT_1:def 9 ;
hence z in a * (Ball (0. X),r) by A4; :: thesis: verum

end;

let z be set ; :: 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:27;
then A8: ||.y1.|| < r by NORMSP_1:6;
||.z1.|| = (abs a) * ||.y1.|| by A6, NORMSP_1:def 2
.= a * ||.y1.|| by A1, ABSVALUE:def 1 ;
then ||.z1.|| < a * r by A1, A8, XREAL_1:70;
then ||.(- z1).|| < a * r by NORMSP_1:6;
then ||.((0. X) - z1).|| < a * r by RLVECT_1:27;
hence z in Ball (0. X),(a * r) ; :: thesis: verum