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