let X, Y be non empty TopSpace; :: thesis: for X0, X1, X2 being non empty SubSpace of X st X1 is SubSpace of X0 & X2 is SubSpace of X1 holds
for g being Function of X0,Y holds (g | X1) | X2 = g | X2
let X0, X1, X2 be non empty SubSpace of X; :: thesis: ( X1 is SubSpace of X0 & X2 is SubSpace of X1 implies for g being Function of X0,Y holds (g | X1) | X2 = g | X2 )
assume A1: ( X1 is SubSpace of X0 & X2 is SubSpace of X1 ) ; :: thesis: for g being Function of X0,Y holds (g | X1) | X2 = g | X2
let g be Function of X0,Y; :: thesis: (g | X1) | X2 = g | X2
set h = g | X1;
A2: g | X1 = g | the carrier of X1 by A1, Def4;
A3: ( the carrier of X1 c= the carrier of X0 & the carrier of X2 c= the carrier of X1 ) by A1, TSEP_1:4;
A4: X2 is SubSpace of X0 by A1, TSEP_1:7;
thus (g | X1) | X2 = (g | X1) | the carrier of X2 by A1, Def4
.= g | the carrier of X2 by A2, A3, FUNCT_1:82
.= g | X2 by A4, Def4 ; :: thesis: verum