let X be LinearTopSpace; :: thesis:
let V be bounded Subset of X; :: thesis:
let r be Real; :: thesis:

per cases ;

suppose A1: r = 0 ; :: thesis:

per cases ;

suppose V is empty ; :: thesis:

hence r * V is bounded by CONVEX1:33; :: thesis:

end;

suppose A2: not V is empty ; :: thesis:

let U be a_neighborhood of 0. X; :: according to RLTOPSP1:def 12 :: thesis:
take s = 1; :: thesis:
thus s > 0 ; :: thesis:
let t be Real; :: thesis:
assume t > s ; :: thesis:
then t * U is a_neighborhood of 0. X by Th55;
then A3: 0. X in t * U by CONNSP_2:4;
r * V = {(0. X)} by A1, A2, CONVEX1:34;
hence r * V c= t * U by A3, ZFMISC_1:31; :: thesis:

end;

end;

end;

suppose A4: r <> 0 ; :: thesis:

let U be a_neighborhood of 0. X; :: according to RLTOPSP1:def 12 :: thesis:
(1 / r) * U is a_neighborhood of 0. X by A4, Th55;
then consider s being Real such that
A5: s > 0 and
A6: for t being Real st t > s holds
V c= t * ((1 / r) * U) by Def12;
take s ; :: thesis:
thus s > 0 by A5; :: thesis:
let t be Real; :: thesis:
assume t > s ; :: thesis:
then r * V c= r * (t * ((1 / r) * U)) by A6, CONVEX1:39;
then r * V c= r * ((t * (1 / r)) * U) by CONVEX1:37;
then r * V c= r * ((1 / r) * (t * U)) by CONVEX1:37;
then r * V c= (r * (1 / r)) * (t * U) by CONVEX1:37;
then r * V c= 1 * (t * U) by A4, XCMPLX_1:87;
then A7: r * V c= t * U by CONVEX1:32;
let x be object ; :: according to TARSKI:def 3 :: thesis:
assume x in r * V ; :: thesis:
hence x in t * U by A7; :: thesis:

end;

end;