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

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