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 SubSpace of X0 holds

for A being Subset of X

for x0 being Point of X0

for x1 being Point of X1 st A is open & x0 in A & A c= the carrier of X1 & 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 SubSpace of X0 holds

for A being Subset of X

for x0 being Point of X0

for x1 being Point of X1 st A is open & x0 in A & A c= the carrier of X1 & 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 SubSpace of X0 implies for A being Subset of X

for x0 being Point of X0

for x1 being Point of X1 st A is open & x0 in A & A c= the carrier of X1 & x0 = x1 holds

( g is_continuous_at x0 iff g | X1 is_continuous_at x1 ) )

assume A1: X1 is SubSpace of X0 ; :: thesis: for A being Subset of X

for x0 being Point of X0

for x1 being Point of X1 st A is open & x0 in A & A c= the carrier of X1 & x0 = x1 holds

( g is_continuous_at x0 iff g | X1 is_continuous_at x1 )

let A be Subset of X; :: thesis: for x0 being Point of X0

for x1 being Point of X1 st A is open & x0 in A & A c= the carrier of X1 & 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 A is open & x0 in A & A c= the carrier of X1 & x0 = x1 holds

( g is_continuous_at x0 iff g | X1 is_continuous_at x1 )

let x1 be Point of X1; :: thesis: ( A is open & x0 in A & A c= the carrier of X1 & x0 = x1 implies ( g is_continuous_at x0 iff g | X1 is_continuous_at x1 ) )

assume that

A2: A is open and

A3: x0 in A and

A4: A c= the carrier of X1 and

A5: x0 = x1 ; :: thesis: ( g is_continuous_at x0 iff g | X1 is_continuous_at x1 )

thus ( g is_continuous_at x0 implies g | X1 is_continuous_at x1 ) by A1, A5, 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

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

for A being Subset of X

for x0 being Point of X0

for x1 being Point of X1 st A is open & x0 in A & A c= the carrier of X1 & 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 SubSpace of X0 holds

for A being Subset of X

for x0 being Point of X0

for x1 being Point of X1 st A is open & x0 in A & A c= the carrier of X1 & 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 SubSpace of X0 implies for A being Subset of X

for x0 being Point of X0

for x1 being Point of X1 st A is open & x0 in A & A c= the carrier of X1 & x0 = x1 holds

( g is_continuous_at x0 iff g | X1 is_continuous_at x1 ) )

assume A1: X1 is SubSpace of X0 ; :: thesis: for A being Subset of X

for x0 being Point of X0

for x1 being Point of X1 st A is open & x0 in A & A c= the carrier of X1 & x0 = x1 holds

( g is_continuous_at x0 iff g | X1 is_continuous_at x1 )

let A be Subset of X; :: thesis: for x0 being Point of X0

for x1 being Point of X1 st A is open & x0 in A & A c= the carrier of X1 & 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 A is open & x0 in A & A c= the carrier of X1 & x0 = x1 holds

( g is_continuous_at x0 iff g | X1 is_continuous_at x1 )

let x1 be Point of X1; :: thesis: ( A is open & x0 in A & A c= the carrier of X1 & x0 = x1 implies ( g is_continuous_at x0 iff g | X1 is_continuous_at x1 ) )

assume that

A2: A is open and

A3: x0 in A and

A4: A c= the carrier of X1 and

A5: x0 = x1 ; :: thesis: ( g is_continuous_at x0 iff g | X1 is_continuous_at x1 )

thus ( g is_continuous_at x0 implies g | X1 is_continuous_at x1 ) by A1, A5, 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 A1, TSEP_1:4;

then reconsider B = A as Subset of X0 by A4, XBOOLE_1:1;

assume A6: g | X1 is_continuous_at x1 ; :: thesis: g is_continuous_at x0

B is open by A2, TOPS_2:25;

hence g is_continuous_at x0 by A1, A3, A4, A5, A6, Th77; :: thesis: verum

end;then reconsider B = A as Subset of X0 by A4, XBOOLE_1:1;

assume A6: g | X1 is_continuous_at x1 ; :: thesis: g is_continuous_at x0

B is open by A2, TOPS_2:25;

hence g is_continuous_at x0 by A1, A3, A4, A5, A6, Th77; :: thesis: verum