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

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