let Y, X 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:94
.= f by FUNCT_2:23 ;
:: thesis: verum