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