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))

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

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 a * (Ball ((0. X),r)) or z in Ball ((0. X),(a * r)) )
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;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

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