( rng f c= I & dom A = I ) by PARTFUN1:def 2;
then dom (A * f) = dom f by RELAT_1:27;
hence for b₁ being dom f -defined Relation st b₁ = A * f holds
b₁ is total by PARTFUN1:def 2; :: thesis: verum