let f be Function of I,J; :: thesis: f is total
dom f = I by FUNCT_2:def 1;
hence f is total by PARTFUN1:def 2; :: thesis: verum