for X, Y being non empty TopSpace
for X0, X1 being non empty SubSpace of X
for f being Function of X,Y st X1 is SubSpace of X0 holds
(f | X0) | X1 = f | X1