the carrier of (Image f) = rng (corestr f) by Th9;
hence corestr f is onto by FUNCT_2:def 3; :: thesis: verum