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