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