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 AS: 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 R1: 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 R1;
then ||.(- z1).|| < a * r by RLVECT_1:27;
then R2: ||.z1.|| < a * r by NORMSP_1:6;
set y1 = (a " ) * z1;
R4: ||.((a " ) * z1).|| = (abs (a " )) * ||.z1.|| by NORMSP_1:def 2
.= (a " ) * ||.z1.|| by AS, ABSVALUE:def 1 ;
(a " ) * ||.z1.|| < (a " ) * (a * r) by R2, AS, XREAL_1:70;
then (a " ) * ||.z1.|| < (a * (a " )) * r ;
then (a " ) * ||.z1.|| < 1 * r by AS, XCMPLX_0:def 7;
then ||.(- ((a " ) * z1)).|| < r by R4, NORMSP_1:6;
then ||.((0. X) - ((a " ) * z1)).|| < r by RLVECT_1:27;
then RA1: (a " ) * z1 in Ball (0. X),r ;
a * ((a " ) * z1) = (a * (a " )) * z1 by RLVECT_1:def 9
.= 1 * z1 by AS, XCMPLX_0:def 7
.= z1 by RLVECT_1:def 9 ;
hence z in a * (Ball (0. X),r) by RA1; :: 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 L1: z in a * (Ball (0. X),r) ; :: thesis: z in Ball (0. X),(a * r)
reconsider z1 = z as Point of X by L1;
consider y1 being Point of X such that
B1: ( z1 = a * y1 & y1 in Ball (0. X),r ) by L1;
ex yy1 being Point of X st
( y1 = yy1 & ||.((0. X) - yy1).|| < r ) by B1;
then ||.(- y1).|| < r by RLVECT_1:27;
then R2: ||.y1.|| < r by NORMSP_1:6;
||.z1.|| = (abs a) * ||.y1.|| by B1, NORMSP_1:def 2
.= a * ||.y1.|| by AS, ABSVALUE:def 1 ;
then ||.z1.|| < a * r by R2, AS, 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