let X be LinearTopSpace; :: thesis: for V being a_neighborhood of 0. X
for r being non zero Real holds r * V is a_neighborhood of 0. X
let V be a_neighborhood of 0. X; :: thesis: for r being non zero Real holds r * V is a_neighborhood of 0. X
let r be non zero Real; :: thesis: r * V is a_neighborhood of 0. X
r * V is a_neighborhood of r * (0. X) by Th54;
hence r * V is a_neighborhood of 0. X ; :: thesis: verum