let X, Y be non empty TopSpace; :: thesis: 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

let X0 be non empty SubSpace of X; :: thesis: 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

let f be Function of X,Y; :: thesis: ( TopStruct(# the carrier of X0, the topology of X0 #) = TopStruct(# the carrier of X, the topology of X #) implies f = f | X0 )

assume TopStruct(# the carrier of X0, the topology of X0 #) = TopStruct(# the carrier of X, the topology of X #) ; :: thesis: f = f | X0

hence f | X0 = f * (id the carrier of X) by RELAT_1:65

.= f by FUNCT_2:17 ;

:: thesis: verum

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

let X0 be non empty SubSpace of X; :: thesis: 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

let f be Function of X,Y; :: thesis: ( TopStruct(# the carrier of X0, the topology of X0 #) = TopStruct(# the carrier of X, the topology of X #) implies f = f | X0 )

assume TopStruct(# the carrier of X0, the topology of X0 #) = TopStruct(# the carrier of X, the topology of X #) ; :: thesis: f = f | X0

hence f | X0 = f * (id the carrier of X) by RELAT_1:65

.= f by FUNCT_2:17 ;

:: thesis: verum