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

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