for X, Y being non empty TopSpace
for X0 being non empty SubSpace of X
for f being Function of X,Y st TopStruct(# the carrier of X0, the topology of X0 #) = TopStruct(# the carrier of X, the topology of X #) holds
f = f | X0