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