let X, Y be non empty TopSpace; :: thesis: for X0 being non empty SubSpace of X
for f being Function of X,Y holds f | X0 = f * (incl X0)
let X0 be non empty SubSpace of X; :: thesis: for f being Function of X,Y holds f | X0 = f * (incl X0)
let f be Function of X,Y; :: thesis: f | X0 = f * (incl X0)
thus f | X0 = (f * (id X)) | X0 by FUNCT_2:17
.= f * (incl X0) by Th62 ; :: thesis: verum