let f be Function of A,B; :: thesis: f is finite
dom f is finite ;
hence f is finite by Th10; :: thesis: verum