let A, B be TopSpace; :: thesis: for f being Function of A,B
for C being Subset of B st f is continuous holds
for h being Function of A,(B | C) st h = f holds
h is continuous
let f be Function of A,B; :: thesis: for C being Subset of B st f is continuous holds
for h being Function of A,(B | C) st h = f holds
h is continuous
let C be Subset of B; :: thesis: ( f is continuous implies for h being Function of A,(B | C) st h = f holds
h is continuous )
assume A1: f is continuous ; :: thesis: for h being Function of A,(B | C) st h = f holds
h is continuous
A2: the carrier of (B | C) = [#] (B | C)
.= C by PRE_TOPC:def 5 ;
let h be Function of A,(B | C); :: thesis: ( h = f implies h is continuous )
assume A3: h = f ; :: thesis: h is continuous
A4: rng f c= the carrier of (B | C) by A3, RELAT_1:def 19;
for P being Subset of (B | C) st P is closed holds
h " P is closed

proof

let P be Subset of (B | C); :: thesis: ( P is closed implies h " P is closed )
assume P is closed ; :: thesis: h " P is closed
then consider Q being Subset of B such that
A5: Q is closed and
A6: Q /\ ([#] (B | C)) = P by PRE_TOPC:13;
h " P = f " (Q /\ C) by A3, A6, PRE_TOPC:def 5
.= (f " Q) /\ (f " C) by FUNCT_1:68
.= (f " Q) /\ (f " ((rng f) /\ C)) by RELAT_1:133
.= (f " Q) /\ (f " (rng f)) by A2, A4, XBOOLE_1:28
.= (f " Q) /\ (dom f) by RELAT_1:134
.= f " Q by RELAT_1:132, XBOOLE_1:28 ;
hence h " P is closed by A1, A5; :: thesis: verum

end;

hence h is continuous ; :: thesis: verum