let X, Y be non empty TopSpace; :: thesis: for X0, X1 being non empty SubSpace of X

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

(f | X0) | X1 = f | X1

let X0, X1 be non empty SubSpace of X; :: thesis: for f being Function of X,Y st X1 is SubSpace of X0 holds

(f | X0) | X1 = f | X1

let f be Function of X,Y; :: thesis: ( X1 is SubSpace of X0 implies (f | X0) | X1 = f | X1 )

assume A1: X1 is SubSpace of X0 ; :: thesis: (f | X0) | X1 = f | X1

then A2: the carrier of X1 c= the carrier of X0 by TSEP_1:4;

f | X0 = f | the carrier of X0 ;

then reconsider h = f | the carrier of X0 as Function of X0,Y ;

thus (f | X0) | X1 = h | the carrier of X1 by A1, Def5

.= f | X1 by A2, FUNCT_1:51 ; :: thesis: verum

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

(f | X0) | X1 = f | X1

let X0, X1 be non empty SubSpace of X; :: thesis: for f being Function of X,Y st X1 is SubSpace of X0 holds

(f | X0) | X1 = f | X1

let f be Function of X,Y; :: thesis: ( X1 is SubSpace of X0 implies (f | X0) | X1 = f | X1 )

assume A1: X1 is SubSpace of X0 ; :: thesis: (f | X0) | X1 = f | X1

then A2: the carrier of X1 c= the carrier of X0 by TSEP_1:4;

f | X0 = f | the carrier of X0 ;

then reconsider h = f | the carrier of X0 as Function of X0,Y ;

thus (f | X0) | X1 = h | the carrier of X1 by A1, Def5

.= f | X1 by A2, FUNCT_1:51 ; :: thesis: verum