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