let f be Function; :: thesis: ( (id ((dom f) \/ (rng f))) * f = f & f * (id ((dom f) \/ (rng f))) = f )
( dom f c= (dom f) \/ (rng f) & rng f c= (dom f) \/ (rng f) ) by XBOOLE_1:7;
hence ( (id ((dom f) \/ (rng f))) * f = f & f * (id ((dom f) \/ (rng f))) = f ) by RELAT_1:77, RELAT_1:79; :: thesis: verum