let A be TopSpace; :: thesis: for B being non empty TopSpace
for f being Function of A,B
for C being SubSpace of B st f is continuous holds
for h being Function of A,C st h = f holds
h is continuous
let B be non empty TopSpace; :: thesis: for f being Function of A,B
for C being SubSpace of B st f is continuous holds
for h being Function of A,C st h = f holds
h is continuous
let f be Function of A,B; :: thesis: for C being SubSpace of B st f is continuous holds
for h being Function of A,C st h = f holds
h is continuous
let C be SubSpace of B; :: thesis: ( f is continuous implies for h being Function of A,C st h = f holds
h is continuous )
assume A1: f is continuous ; :: thesis: for h being Function of A,C st h = f holds
h is continuous
let h be Function of A,C; :: thesis: ( h = f implies h is continuous )
assume A2: h = f ; :: thesis: h is continuous
A3: rng f c= the carrier of C by A2, RELAT_1:def 19;
for P being Subset of C st P is closed holds
h " P is closed

proof

let P be Subset of 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
A4: ( Q is closed & Q /\ ([#] C) = P ) by Th43;
A5: ( f " Q c= dom f & the carrier of A = [#] A & dom f = the carrier of A ) by FUNCT_2:def 1, RELAT_1:167;
h " P = (f " Q) /\ (f " ([#] C)) by A2, A4, FUNCT_1:137
.= (f " Q) /\ (f " ((rng f) /\ ([#] C))) by RELAT_1:168
.= (f " Q) /\ (f " (rng f)) by A3, XBOOLE_1:28
.= (f " Q) /\ (dom f) by RELAT_1:169
.= f " Q by A5, XBOOLE_1:28 ;
hence h " P is closed by A1, A4, Def12; :: thesis: verum

end;

hence h is continuous by Def12; :: thesis: verum