for X, Y being RealNormSpace
for f being PartFunc of X,Y
for A being Subset of X
for B being Subset of Y st dom f = A & f is_continuous_on A & A is open & B is open holds
f " B is open