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
(mlt r,X) .: V = r * V by Th47;
hence r * V is open by TOPGRP_1:25; :: thesis: verum