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