let X, Y be non empty TopSpace; :: thesis: for f being Function of X,Y st f is continuous holds
corestr f is continuous
let f be Function of X,Y; :: thesis: ( f is continuous implies corestr f is continuous )
A1: f is Function of (dom f),(rng f) by FUNCT_2:1;
A2: [#] Y <> {} ;
assume A3: f is continuous ; :: thesis: corestr f is continuous
A4: for R being Subset of (Image f) st R is open holds
(corestr f) " R is open

proof

[#] (Image f) = rng f by Th9;
then A5: f " ([#] (Image f)) = dom f by A1, FUNCT_2:40
.= the carrier of X by FUNCT_2:def 1 ;
the carrier of X in the topology of X by PRE_TOPC:def 1;
then A6: f " ([#] (Image f)) is open by A5;
let R be Subset of (Image f); :: thesis: ( R is open implies (corestr f) " R is open )
assume R is open ; :: thesis: (corestr f) " R is open
then R in the topology of (Image f) ;
then consider Q being Subset of Y such that
A7: Q in the topology of Y and
A8: R = Q /\ ([#] (Image f)) by PRE_TOPC:def 4;
reconsider Q = Q as Subset of Y ;
Q is open by A7;
then A9: f " Q is open by A3, A2, TOPS_2:43;
(f " Q) /\ (f " ([#] (Image f))) = f " (Q /\ ([#] (Image f))) by FUNCT_1:68;
hence (corestr f) " R is open by A8, A9, A6, TOPS_1:11; :: thesis: verum

end;

[#] (Image f) <> {} ;
hence corestr f is continuous by A4, TOPS_2:43; :: thesis: verum