let X, Y be non empty TopSpace; :: thesis: for X0, X1 being non empty SubSpace of X
for g being Function of X0,Y st X1 is SubSpace of X0 holds
for B being Subset of Y st g " B c= the carrier of X1 holds
g " B = (g | X1) " B
let X0, X1 be non empty SubSpace of X; :: thesis: for g being Function of X0,Y st X1 is SubSpace of X0 holds
for B being Subset of Y st g " B c= the carrier of X1 holds
g " B = (g | X1) " B
let g be Function of X0,Y; :: thesis: ( X1 is SubSpace of X0 implies for B being Subset of Y st g " B c= the carrier of X1 holds
g " B = (g | X1) " B )
assume A1: X1 is SubSpace of X0 ; :: thesis: for B being Subset of Y st g " B c= the carrier of X1 holds
g " B = (g | X1) " B
let B be Subset of Y; :: thesis: ( g " B c= the carrier of X1 implies g " B = (g | X1) " B )
assume g " B c= the carrier of X1 ; :: thesis: g " B = (g | X1) " B
hence g " B = (g | the carrier of X1) " B by FUNCT_2:98
.= (g | X1) " B by A1, Def5 ;
:: thesis: verum