let X, Y be non empty TopSpace; :: thesis: for X0, X1 being non empty SubSpace of X
for f being Function of X,Y
for g being Function of X0,Y st g = f | X0 & X1 is SubSpace of X0 holds
g | X1 = f | X1
let X0, X1 be non empty SubSpace of X; :: thesis: for f being Function of X,Y
for g being Function of X0,Y st g = f | X0 & X1 is SubSpace of X0 holds
g | X1 = f | X1
let f be Function of X,Y; :: thesis: for g being Function of X0,Y st g = f | X0 & X1 is SubSpace of X0 holds
g | X1 = f | X1
let g be Function of X0,Y; :: thesis: ( g = f | X0 & X1 is SubSpace of X0 implies g | X1 = f | X1 )
assume A1: g = f | X0 ; :: thesis: ( not X1 is SubSpace of X0 or g | X1 = f | X1 )
assume A2: X1 is SubSpace of X0 ; :: thesis: g | X1 = f | X1
then A3: the carrier of X1 c= the carrier of X0 by TSEP_1:4;
thus g | X1 = g | the carrier of X1 by A2, Def5
.= f | X1 by A1, A3, FUNCT_1:51 ; :: thesis: verum