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 g1 being Function of X1,Y st ( for x0 being Point of X0 st x0 in the carrier of X1 holds

g . x0 = g1 . x0 ) holds

g | X1 = g1

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 g1 being Function of X1,Y st ( for x0 being Point of X0 st x0 in the carrier of X1 holds

g . x0 = g1 . x0 ) holds

g | X1 = g1

let g be Function of X0,Y; :: thesis: ( X1 is SubSpace of X0 implies for g1 being Function of X1,Y st ( for x0 being Point of X0 st x0 in the carrier of X1 holds

g . x0 = g1 . x0 ) holds

g | X1 = g1 )

assume A1: X1 is SubSpace of X0 ; :: thesis: for g1 being Function of X1,Y st ( for x0 being Point of X0 st x0 in the carrier of X1 holds

g . x0 = g1 . x0 ) holds

g | X1 = g1

then A2: the carrier of X1 is Subset of X0 by TSEP_1:1;

let g1 be Function of X1,Y; :: thesis: ( ( for x0 being Point of X0 st x0 in the carrier of X1 holds

g . x0 = g1 . x0 ) implies g | X1 = g1 )

assume for x0 being Point of X0 st x0 in the carrier of X1 holds

g . x0 = g1 . x0 ; :: thesis: g | X1 = g1

then g | the carrier of X1 = g1 by A2, FUNCT_2:96;

hence g | X1 = g1 by A1, Def5; :: thesis: verum

for g being Function of X0,Y st X1 is SubSpace of X0 holds

for g1 being Function of X1,Y st ( for x0 being Point of X0 st x0 in the carrier of X1 holds

g . x0 = g1 . x0 ) holds

g | X1 = g1

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 g1 being Function of X1,Y st ( for x0 being Point of X0 st x0 in the carrier of X1 holds

g . x0 = g1 . x0 ) holds

g | X1 = g1

let g be Function of X0,Y; :: thesis: ( X1 is SubSpace of X0 implies for g1 being Function of X1,Y st ( for x0 being Point of X0 st x0 in the carrier of X1 holds

g . x0 = g1 . x0 ) holds

g | X1 = g1 )

assume A1: X1 is SubSpace of X0 ; :: thesis: for g1 being Function of X1,Y st ( for x0 being Point of X0 st x0 in the carrier of X1 holds

g . x0 = g1 . x0 ) holds

g | X1 = g1

then A2: the carrier of X1 is Subset of X0 by TSEP_1:1;

let g1 be Function of X1,Y; :: thesis: ( ( for x0 being Point of X0 st x0 in the carrier of X1 holds

g . x0 = g1 . x0 ) implies g | X1 = g1 )

assume for x0 being Point of X0 st x0 in the carrier of X1 holds

g . x0 = g1 . x0 ; :: thesis: g | X1 = g1

then g | the carrier of X1 = g1 by A2, FUNCT_2:96;

hence g | X1 = g1 by A1, Def5; :: thesis: verum