let TX, TY be non empty TopSpace; :: thesis: for P being non empty Subset of TY

for f being Function of TX,(TY | P) holds

( f is Function of TX,TY & ( for f2 being Function of TX,TY st f2 = f & f is continuous holds

f2 is continuous ) )

let P be non empty Subset of TY; :: thesis: for f being Function of TX,(TY | P) holds

( f is Function of TX,TY & ( for f2 being Function of TX,TY st f2 = f & f is continuous holds

f2 is continuous ) )

let f be Function of TX,(TY | P); :: thesis: ( f is Function of TX,TY & ( for f2 being Function of TX,TY st f2 = f & f is continuous holds

f2 is continuous ) )

A1: the carrier of (TY | P) = [#] (TY | P)

.= P by PRE_TOPC:def 5 ;

hence f is Function of TX,TY by FUNCT_2:7; :: thesis: for f2 being Function of TX,TY st f2 = f & f is continuous holds

f2 is continuous

let f2 be Function of TX,TY; :: thesis: ( f2 = f & f is continuous implies f2 is continuous )

assume that

A2: f2 = f and

A3: f is continuous ; :: thesis: f2 is continuous

let P1 be Subset of TY; :: according to PRE_TOPC:def 6 :: thesis: ( not P1 is closed or f2 " P1 is closed )

assume A4: P1 is closed ; :: thesis: f2 " P1 is closed

reconsider P3 = P1 /\ P as Subset of (TY | P) by TOPS_2:29;

A5: P3 is closed by A4, Th2;

f2 " P = the carrier of TX by A1, A2, FUNCT_2:40

.= dom f2 by FUNCT_2:def 1 ;

then f2 " P1 = (f2 " P1) /\ (f2 " P) by RELAT_1:132, XBOOLE_1:28

.= f " P3 by A2, FUNCT_1:68 ;

hence f2 " P1 is closed by A3, A5; :: thesis: verum

for f being Function of TX,(TY | P) holds

( f is Function of TX,TY & ( for f2 being Function of TX,TY st f2 = f & f is continuous holds

f2 is continuous ) )

let P be non empty Subset of TY; :: thesis: for f being Function of TX,(TY | P) holds

( f is Function of TX,TY & ( for f2 being Function of TX,TY st f2 = f & f is continuous holds

f2 is continuous ) )

let f be Function of TX,(TY | P); :: thesis: ( f is Function of TX,TY & ( for f2 being Function of TX,TY st f2 = f & f is continuous holds

f2 is continuous ) )

A1: the carrier of (TY | P) = [#] (TY | P)

.= P by PRE_TOPC:def 5 ;

hence f is Function of TX,TY by FUNCT_2:7; :: thesis: for f2 being Function of TX,TY st f2 = f & f is continuous holds

f2 is continuous

let f2 be Function of TX,TY; :: thesis: ( f2 = f & f is continuous implies f2 is continuous )

assume that

A2: f2 = f and

A3: f is continuous ; :: thesis: f2 is continuous

let P1 be Subset of TY; :: according to PRE_TOPC:def 6 :: thesis: ( not P1 is closed or f2 " P1 is closed )

assume A4: P1 is closed ; :: thesis: f2 " P1 is closed

reconsider P3 = P1 /\ P as Subset of (TY | P) by TOPS_2:29;

A5: P3 is closed by A4, Th2;

f2 " P = the carrier of TX by A1, A2, FUNCT_2:40

.= dom f2 by FUNCT_2:def 1 ;

then f2 " P1 = (f2 " P1) /\ (f2 " P) by RELAT_1:132, XBOOLE_1:28

.= f " P3 by A2, FUNCT_1:68 ;

hence f2 " P1 is closed by A3, A5; :: thesis: verum