let X be LinearTopSpace; :: thesis: for V being open Subset of X
for r being non zero Real holds r * V is open
let V be open Subset of X; :: thesis: for r being non zero Real holds r * V is open
let r be non zero Real; :: thesis: r * V is open
reconsider r = r as non zero Real ;
(mlt (r,X)) .: V = r * V by Th46;
hence r * V is open by TOPGRP_1:25; :: thesis: verum