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