take I --> 1 ; :: thesis: I --> 1 is total
dom (I --> 1) = I by Th19;
hence I --> 1 is total by PARTFUN1:def 4; :: thesis: verum