dom (Carrier C) = I by PARTFUN1:def 2;
hence Carrier C is ManySortedSet of I ; :: thesis: verum