theorem Th7: :: INSTALG1:7

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