take I --> {} ; :: thesis: dom (I --> {} ) = I
thus dom (I --> {} ) = I by FUNCOP_1:19; :: thesis: verum