theorem :: TMAP_1:55

for X, Y being non empty TopSpace
for X0 being non empty SubSpace of X
for f being Function of X,Y
for A being Subset of X st A c= the carrier of X0 holds
f .: A = (f | X0) .: A by FUNCT_2:97;