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 )
assume A1: f is continuous ; :: thesis: corestr f is continuous
A2: f is Function of (dom f),(rng f) by FUNCT_2:3;
A3: ( [#] Y <> {} & [#] (Image f) <> {} ) ;
for R being Subset of (Image f) st R is open holds
(corestr f) " R is open

proof

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) by PRE_TOPC:def 5;
then consider Q being Subset of Y such that
A4: Q in the topology of Y and
A5: R = Q /\ ([#] (Image f)) by PRE_TOPC:def 9;
reconsider Q = Q as Subset of Y ;
Q is open by A4, PRE_TOPC:def 5;
then A6: f " Q is open by A1, A3, TOPS_2:55;
[#] (Image f) = rng f by Th10;
then A7: f " ([#] (Image f)) = dom f by A2, FUNCT_2:48
.= the carrier of X by FUNCT_2:def 1 ;
the carrier of X in the topology of X by PRE_TOPC:def 1;
then A8: f " ([#] (Image f)) is open by A7, PRE_TOPC:def 5;
(f " Q) /\ (f " ([#] (Image f))) = f " (Q /\ ([#] (Image f))) by FUNCT_1:137;
hence (corestr f) " R is open by A5, A6, A8, TOPS_1:38; :: thesis: verum

end;

hence corestr f is continuous by A3, TOPS_2:55; :: thesis: verum