let X be LinearTopSpace; :: thesis: for V being bounded Subset of X
for r being Real holds r * V is bounded
let V be bounded Subset of X; :: thesis: for r being Real holds r * V is bounded
let r be Real; :: thesis: r * V is bounded

per cases ( r = 0 or r <> 0 ) ;

suppose A1: r = 0 ; :: thesis: r * V is bounded

per cases ( V is empty or not V is empty ) ;

suppose V is empty ; :: thesis: r * V is bounded

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

end;

suppose A2: not V is empty ; :: thesis: r * V is bounded

let U be a_neighborhood of 0. X; :: according to RLTOPSP1:def 12 :: thesis: ex s being Real st
( s > 0 & ( for t being Real st t > s holds
r * V c= t * U ) )
take s = 1; :: thesis: ( s > 0 & ( for t being Real st t > s holds
r * V c= t * U ) )
thus s > 0 ; :: thesis: for t being Real st t > s holds
r * V c= t * U
let t be Real; :: thesis: ( t > s implies r * V c= t * U )
assume t > s ; :: thesis: r * V c= t * U
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: verum

end;

end;

end;

suppose A4: r <> 0 ; :: thesis: r * V is bounded

let U be a_neighborhood of 0. X; :: according to RLTOPSP1:def 12 :: thesis: ex s being Real st
( s > 0 & ( for t being Real st t > s holds
r * V c= t * U ) )
(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: ( s > 0 & ( for t being Real st t > s holds
r * V c= t * U ) )
thus s > 0 by A5; :: thesis: for t being Real st t > s holds
r * V c= t * U
let t be Real; :: thesis: ( t > s implies r * V c= t * U )
assume t > s ; :: thesis: r * V c= t * U
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: ( not x in r * V or x in t * U )
assume x in r * V ; :: thesis: x in t * U
hence x in t * U by A7; :: thesis: verum

end;

end;