for X being RealNormSpace
for U being Subset of (TopSpaceNorm X)
for Ut being Subset of (LinearTopSpaceNorm X)
for x being Point of (TopSpaceNorm X)
for xt being Point of (LinearTopSpaceNorm X) st U = Ut & x = xt holds
( U is a_neighborhood of x iff Ut is a_neighborhood of xt )