for X, Y being non empty TopSpace
for X0, X1 being non empty SubSpace of X
for g being Function of X0,Y st X1 is SubSpace of X0 holds
for B being Subset of Y st g " B c= the carrier of X1 holds
g " B = (g | X1) " B