let X, Y be non empty TopSpace; :: thesis: for X0 being non empty SubSpace of X

for g being Function of X0,Y holds g = g | X0

let X0 be non empty SubSpace of X; :: thesis: for g being Function of X0,Y holds g = g | X0

let g be Function of X0,Y; :: thesis: g = g | X0

X0 is SubSpace of X0 by TSEP_1:2;

hence g | X0 = g | the carrier of X0 by Def5

.= g * (id the carrier of X0) by RELAT_1:65

.= g by FUNCT_2:17 ;

:: thesis: verum

for g being Function of X0,Y holds g = g | X0

let X0 be non empty SubSpace of X; :: thesis: for g being Function of X0,Y holds g = g | X0

let g be Function of X0,Y; :: thesis: g = g | X0

X0 is SubSpace of X0 by TSEP_1:2;

hence g | X0 = g | the carrier of X0 by Def5

.= g * (id the carrier of X0) by RELAT_1:65

.= g by FUNCT_2:17 ;

:: thesis: verum