take I --> {} ; :: thesis: I --> {} is total
dom (I --> {} ) = I by FUNCOP_1:19;
hence I --> {} is total by PARTFUN1:def 4; :: thesis: verum