for X, Y being RealNormSpace
for L being Function of X,Y
for w being Point of Y st L is_continuous_on the carrier of X holds
L " {w} is closed