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 x0 being Point of X0 st x0 in the carrier of X1 holds
g . x0 = (g | X1) . x0
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 x0 being Point of X0 st x0 in the carrier of X1 holds
g . x0 = (g | X1) . x0
let g be Function of X0,Y; :: thesis: ( X1 is SubSpace of X0 implies for x0 being Point of X0 st x0 in the carrier of X1 holds
g . x0 = (g | X1) . x0 )
assume A1: X1 is SubSpace of X0 ; :: thesis: for x0 being Point of X0 st x0 in the carrier of X1 holds
g . x0 = (g | X1) . x0
let x0 be Point of X0; :: thesis: ( x0 in the carrier of X1 implies g . x0 = (g | X1) . x0 )
assume x0 in the carrier of X1 ; :: thesis: g . x0 = (g | X1) . x0
hence g . x0 = (g | the carrier of X1) . x0 by FUNCT_1:49
.= (g | X1) . x0 by A1, Def5 ;
:: thesis: verum