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