( rng f c= I & dom A = I ) by PARTFUN1:def 2;
then dom (A * f) = dom f by RELAT_1:27;
hence A * f is dom f -defined by RELAT_1:def 18; :: thesis: verum