let X, Y be non empty TopSpace; :: thesis: for X1, X0 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 X1, X0 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
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 A2: for x0 being Point of X0 st x0 in the carrier of X1 holds
g . x0 = g1 . x0 ; :: thesis: g | X1 = g1
the carrier of X1 is Subset of X0 by A1, TSEP_1:1;
then g | the carrier of X1 = g1 by A2, FUNCT_2:173;
hence g | X1 = g1 by A1, Def4; :: thesis: verum