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

for f being Function of X,Y st X1 is SubSpace of X0 holds

for x0 being Point of X0

for x1 being Point of X1 st x0 = x1 & f | X0 is_continuous_at x0 holds

f | X1 is_continuous_at x1

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

for x0 being Point of X0

for x1 being Point of X1 st x0 = x1 & f | X0 is_continuous_at x0 holds

f | X1 is_continuous_at x1

let f be Function of X,Y; :: thesis: ( X1 is SubSpace of X0 implies for x0 being Point of X0

for x1 being Point of X1 st x0 = x1 & f | X0 is_continuous_at x0 holds

f | X1 is_continuous_at x1 )

assume A1: X1 is SubSpace of X0 ; :: thesis: for x0 being Point of X0

for x1 being Point of X1 st x0 = x1 & f | X0 is_continuous_at x0 holds

f | X1 is_continuous_at x1

let x0 be Point of X0; :: thesis: for x1 being Point of X1 st x0 = x1 & f | X0 is_continuous_at x0 holds

f | X1 is_continuous_at x1

let x1 be Point of X1; :: thesis: ( x0 = x1 & f | X0 is_continuous_at x0 implies f | X1 is_continuous_at x1 )

assume A2: x0 = x1 ; :: thesis: ( not f | X0 is_continuous_at x0 or f | X1 is_continuous_at x1 )

assume f | X0 is_continuous_at x0 ; :: thesis: f | X1 is_continuous_at x1

then (f | X0) | X1 is_continuous_at x1 by A1, A2, Th74;

hence f | X1 is_continuous_at x1 by A1, Th71; :: thesis: verum

for f being Function of X,Y st X1 is SubSpace of X0 holds

for x0 being Point of X0

for x1 being Point of X1 st x0 = x1 & f | X0 is_continuous_at x0 holds

f | X1 is_continuous_at x1

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

for x0 being Point of X0

for x1 being Point of X1 st x0 = x1 & f | X0 is_continuous_at x0 holds

f | X1 is_continuous_at x1

let f be Function of X,Y; :: thesis: ( X1 is SubSpace of X0 implies for x0 being Point of X0

for x1 being Point of X1 st x0 = x1 & f | X0 is_continuous_at x0 holds

f | X1 is_continuous_at x1 )

assume A1: X1 is SubSpace of X0 ; :: thesis: for x0 being Point of X0

for x1 being Point of X1 st x0 = x1 & f | X0 is_continuous_at x0 holds

f | X1 is_continuous_at x1

let x0 be Point of X0; :: thesis: for x1 being Point of X1 st x0 = x1 & f | X0 is_continuous_at x0 holds

f | X1 is_continuous_at x1

let x1 be Point of X1; :: thesis: ( x0 = x1 & f | X0 is_continuous_at x0 implies f | X1 is_continuous_at x1 )

assume A2: x0 = x1 ; :: thesis: ( not f | X0 is_continuous_at x0 or f | X1 is_continuous_at x1 )

assume f | X0 is_continuous_at x0 ; :: thesis: f | X1 is_continuous_at x1

then (f | X0) | X1 is_continuous_at x1 by A1, A2, Th74;

hence f | X1 is_continuous_at x1 by A1, Th71; :: thesis: verum