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 st g | X1 is continuous Function of X1,Y holds

g | X2 is continuous Function of X2,Y

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 st g | X1 is continuous Function of X1,Y holds

g | X2 is continuous Function of X2,Y )

assume A1: X1 is SubSpace of X0 ; :: thesis: ( not X2 is SubSpace of X1 or for g being Function of X0,Y st g | X1 is continuous Function of X1,Y holds

g | X2 is continuous Function of X2,Y )

assume A2: X2 is SubSpace of X1 ; :: thesis: for g being Function of X0,Y st g | X1 is continuous Function of X1,Y holds

g | X2 is continuous Function of X2,Y

let g be Function of X0,Y; :: thesis: ( g | X1 is continuous Function of X1,Y implies g | X2 is continuous Function of X2,Y )

assume g | X1 is continuous Function of X1,Y ; :: thesis: g | X2 is continuous Function of X2,Y

then (g | X1) | X2 is continuous Function of X2,Y by A2, Th82;

hence g | X2 is continuous Function of X2,Y by A1, A2, Th72; :: thesis: verum

for g being Function of X0,Y st g | X1 is continuous Function of X1,Y holds

g | X2 is continuous Function of X2,Y

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 st g | X1 is continuous Function of X1,Y holds

g | X2 is continuous Function of X2,Y )

assume A1: X1 is SubSpace of X0 ; :: thesis: ( not X2 is SubSpace of X1 or for g being Function of X0,Y st g | X1 is continuous Function of X1,Y holds

g | X2 is continuous Function of X2,Y )

assume A2: X2 is SubSpace of X1 ; :: thesis: for g being Function of X0,Y st g | X1 is continuous Function of X1,Y holds

g | X2 is continuous Function of X2,Y

let g be Function of X0,Y; :: thesis: ( g | X1 is continuous Function of X1,Y implies g | X2 is continuous Function of X2,Y )

assume g | X1 is continuous Function of X1,Y ; :: thesis: g | X2 is continuous Function of X2,Y

then (g | X1) | X2 is continuous Function of X2,Y by A2, Th82;

hence g | X2 is continuous Function of X2,Y by A1, A2, Th72; :: thesis: verum