theorem Th18: :: NORMSP_2:18

for X, Y being RealNormSpace
for f being PartFunc of X,Y
for ft being Function of (TopSpaceNorm X),(TopSpaceNorm Y)
for x being Point of X
for xt being Point of (TopSpaceNorm X) st f = ft & x = xt holds
( f is_continuous_in x iff ft is_continuous_at xt )