J c= I ;
then J c= dom F by PARTFUN1:def 2;
then dom (F | J) = J by RELAT_1:62;
hence ( F | J is J -defined & F | J is total ) by PARTFUN1:def 2; :: thesis: verum