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

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

hence
h is continuous
; :: thesis: verum
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;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