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 A being Subset of X0 st A c= the carrier of X1 holds
g .: A = (g | X1) .: A
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 A being Subset of X0 st A c= the carrier of X1 holds
g .: A = (g | X1) .: A
let g be Function of X0,Y; :: thesis: ( X1 is SubSpace of X0 implies for A being Subset of X0 st A c= the carrier of X1 holds
g .: A = (g | X1) .: A )
assume A1: X1 is SubSpace of X0 ; :: thesis: for A being Subset of X0 st A c= the carrier of X1 holds
g .: A = (g | X1) .: A
let A be Subset of X0; :: thesis: ( A c= the carrier of X1 implies g .: A = (g | X1) .: A )
assume A c= the carrier of X1 ; :: thesis: g .: A = (g | X1) .: A
hence g .: A = (g | the carrier of X1) .: A by FUNCT_2:97
.= (g | X1) .: A by A1, Def5 ;
:: thesis: verum