let TX, TY be non empty TopSpace; 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; 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); ( 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; for f2 being Function of TX,TY st f2 = f & f is continuous holds
f2 is continuous
let f2 be Function of TX,TY; ( f2 = f & f is continuous implies f2 is continuous )
assume that
A2:
f2 = f
and
A3:
f is continuous
; f2 is continuous
let P1 be Subset of TY; PRE_TOPC:def 6 ( not P1 is closed or f2 " P1 is closed )
assume A4:
P1 is closed
; 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; verum