:: deftheorem Def5 defines | TMAP_1:def 5 :
for X, Y being non empty TopSpace
for X0, X1 being SubSpace of X
for g being Function of X0,Y st X1 is SubSpace of X0 holds
g | X1 = g | the carrier of X1;