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