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

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