let L1, L2 be non empty RelStr ; :: thesis: for g being Function of L1,L2 holds corestr g is onto
let g be Function of L1,L2; :: thesis: corestr g is onto
the carrier of (Image g) = rng g by YELLOW_0:def 15
.= rng (corestr g) by Th30 ;
hence corestr g is onto by FUNCT_2:def 3; :: thesis: verum