let L be non empty RelStr ; :: thesis: for f being Function of L,L holds (inclusion f) * (corestr f) = f
let f be Function of L,L; :: thesis: (inclusion f) * (corestr f) = f
thus (inclusion f) * (corestr f) = (id the carrier of (Image f)) * f by Th30
.= (id (rng f)) * f by YELLOW_0:def 15
.= f by RELAT_1:54 ; :: thesis: verum