A1: dom A = J by PARTFUN1:def 2;
dom (Carrier A) = dom A by Def13;
hence Carrier A is ManySortedSet of J by A1, RELAT_1:def 18, PARTFUN1:def 2; :: thesis: verum