for S being ManySortedSign holds
( S is feasible iff dom the ResultSort of S = the carrier' of S ) by FUNCT_2:def 1;