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