for X being RealUnitarySpace
for w being Point of X
for f being Function of X,REAL st ( for v being Point of X holds f . v = w .|. v ) holds
f is_continuous_on the carrier of X