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 x0 being Point of X0 st x0 in the carrier of X1 holds
g . x0 = (g | X1) . x0