:: deftheorem defines | TMAP_1:def 4 :
for X, Y being non empty TopSpace
for f being Function of X,Y
for X0 being SubSpace of X holds f | X0 = f | the carrier of X0;