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 that
A1: X1 is SubSpace of X0 and
A2: X2 is SubSpace of X1 ; :: thesis: for g being Function of X0,Y holds (g | X1) | X2 = g | X2
A3: X2 is SubSpace of X0 by A1, A2, TSEP_1:7;
let g be Function of X0,Y; :: thesis: (g | X1) | X2 = g | X2
set h = g | X1;
A4: ( g | X1 = g | the carrier of X1 & the carrier of X2 c= the carrier of X1 ) by A1, A2, Def5, TSEP_1:4;
thus (g | X1) | X2 = (g | X1) | the carrier of X2 by A2, Def5
.= g | the carrier of X2 by A4, FUNCT_1:51
.= g | X2 by A3, Def5 ; :: thesis: verum