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 and
A5: Q /\ ([#] C) = P by Th13;
h " P = (f " Q) /\ (f " ([#] C)) by A2, A5, FUNCT_1:68
.= (f " Q) /\ (f " ((rng f) /\ ([#] C))) by RELAT_1:133
.= (f " Q) /\ (f " (rng f)) by A3, 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, A4; :: thesis: verum
end;
hence h is continuous ; :: thesis: verum