theorem :: TMAP_1:73

for X, Y being non empty TopSpace
for X0, X1 being non empty SubSpace of X
for f being Function of X,Y
for f0 being Function of X1,Y
for g being Function of X0,Y st X0 = X & f = g holds
( g | X1 = f0 iff f | X1 = f0 ) by Def5;