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

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