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

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