let X, Y be non empty TopSpace; :: thesis: for X0, X1 being non empty SubSpace of X

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

g | X1 is continuous Function of X1,Y

let X0, X1 be non empty SubSpace of X; :: thesis: for g being continuous Function of X0,Y st X1 is SubSpace of X0 holds

g | X1 is continuous Function of X1,Y

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

assume A1: X1 is SubSpace of X0 ; :: thesis: g | X1 is continuous Function of X1,Y

for x1 being Point of X1 holds g | X1 is_continuous_at x1

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

g | X1 is continuous Function of X1,Y

let X0, X1 be non empty SubSpace of X; :: thesis: for g being continuous Function of X0,Y st X1 is SubSpace of X0 holds

g | X1 is continuous Function of X1,Y

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

assume A1: X1 is SubSpace of X0 ; :: thesis: g | X1 is continuous Function of X1,Y

for x1 being Point of X1 holds g | X1 is_continuous_at x1

proof

hence
g | X1 is continuous Function of X1,Y
by Th44; :: thesis: verum
let x1 be Point of X1; :: thesis: g | X1 is_continuous_at x1

consider x0 being Point of X0 such that

A2: x0 = x1 by A1, Th10;

g is_continuous_at x0 by Th44;

hence g | X1 is_continuous_at x1 by A1, A2, Th74; :: thesis: verum

end;consider x0 being Point of X0 such that

A2: x0 = x1 by A1, Th10;

g is_continuous_at x0 by Th44;

hence g | X1 is_continuous_at x1 by A1, A2, Th74; :: thesis: verum