set g = corestr f;
A1: dom (corestr f) = [#] X by FUNCT_2:def 1;
rng (corestr f) = [#] (Image f) by FUNCT_2:def 3;
then (corestr f) .: ([#] X) = [#] (Image f) by A1, RELAT_1:113;
hence Image f is connected by CONNSP_1:14, WAYBEL18:10; :: thesis: verum