let X be LinearTopSpace; :: thesis: for V being Subset of X
for r being non zero Real holds r * (Int V) = Int (r * V)
let V be Subset of X; :: thesis: for r being non zero Real holds r * (Int V) = Int (r * V)
let r be non zero Real; :: thesis: r * (Int V) = Int (r * V)
r * (Int V) c= r * V by CONVEX1:39, TOPS_1:16;
hence r * (Int V) c= Int (r * V) by Th49, TOPS_1:24; :: according to XBOOLE_0:def 10 :: thesis: Int (r * V) c= r * (Int V)
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in Int (r * V) or x in r * (Int V) )
assume A1: x in Int (r * V) ; :: thesis: x in r * (Int V)
then reconsider x = x as Point of X ;
consider Q being Subset of X such that
A2: Q is open and
A3: Q c= r * V and
A4: x in Q by A1, TOPS_1:22;
(r ") * Q c= (r ") * (r * V) by A3, CONVEX1:39;
then (r ") * Q c= ((r ") * r) * V by CONVEX1:37;
then (r ") * Q c= 1 * V by XCMPLX_0:def 7;
then A5: (r ") * Q c= V by CONVEX1:32;
( (r ") * x in (r ") * Q & (r ") * Q is open ) by A2, A4, Th49;
then (r ") * x in Int V by A5, TOPS_1:22;
then r * ((r ") * x) in r * (Int V) ;
then (r * (r ")) * x in r * (Int V) by RLVECT_1:def 7;
then 1 * x in r * (Int V) by XCMPLX_0:def 7;
hence x in r * (Int V) by RLVECT_1:def 8; :: thesis: verum