theorem :: TMAP_1:86

for X, Y being non empty TopSpace
for X0 being non empty SubSpace of X
for f being Function of X,Y holds f | X0 = f * (incl X0)