let X, Y be non empty TopSpace; :: thesis: for X0, X1 being non empty SubSpace of X
for g being Function of X0,Y st X1 is open SubSpace of X & X1 is SubSpace of X0 holds
for x0 being Point of X0
for x1 being Point of X1 st x0 = x1 holds
( g is_continuous_at x0 iff g | X1 is_continuous_at x1 )
let X0, X1 be non empty SubSpace of X; :: thesis: for g being Function of X0,Y st X1 is open SubSpace of X & X1 is SubSpace of X0 holds
for x0 being Point of X0
for x1 being Point of X1 st x0 = x1 holds
( g is_continuous_at x0 iff g | X1 is_continuous_at x1 )
let g be Function of X0,Y; :: thesis: ( X1 is open SubSpace of X & X1 is SubSpace of X0 implies for x0 being Point of X0
for x1 being Point of X1 st x0 = x1 holds
( g is_continuous_at x0 iff g | X1 is_continuous_at x1 ) )
assume A1: X1 is open SubSpace of X ; :: thesis: ( not X1 is SubSpace of X0 or for x0 being Point of X0
for x1 being Point of X1 st x0 = x1 holds
( g is_continuous_at x0 iff g | X1 is_continuous_at x1 ) )
assume A2: X1 is SubSpace of X0 ; :: thesis: for x0 being Point of X0
for x1 being Point of X1 st x0 = x1 holds
( g is_continuous_at x0 iff g | X1 is_continuous_at x1 )
let x0 be Point of X0; :: thesis: for x1 being Point of X1 st x0 = x1 holds
( g is_continuous_at x0 iff g | X1 is_continuous_at x1 )
let x1 be Point of X1; :: thesis: ( x0 = x1 implies ( g is_continuous_at x0 iff g | X1 is_continuous_at x1 ) )
assume A3: x0 = x1 ; :: thesis: ( g is_continuous_at x0 iff g | X1 is_continuous_at x1 )
hence ( g is_continuous_at x0 implies g | X1 is_continuous_at x1 ) by A2, Th74; :: thesis: ( g | X1 is_continuous_at x1 implies g is_continuous_at x0 )
thus ( g | X1 is_continuous_at x1 implies g is_continuous_at x0 ) :: thesis: verum

proof

the carrier of X1 c= the carrier of X0 by A2, TSEP_1:4;
then A4: X1 is open SubSpace of X0 by A1, TSEP_1:19;
assume g | X1 is_continuous_at x1 ; :: thesis: g is_continuous_at x0
hence g is_continuous_at x0 by A3, A4, Th79; :: thesis: verum

end;