let S be ManySortedSign ; :: thesis: ( S is feasible iff dom the ResultSort of S = the carrier' of S )

hereby :: thesis: ( dom the ResultSort of S = the carrier' of S implies S is feasible )

assume S is feasible ; :: thesis: dom the ResultSort of S = the carrier' of S
then ( the carrier of S = {} implies the carrier' of S = {} ) by Def1;
hence dom the ResultSort of S = the carrier' of S by FUNCT_2:def 1; :: thesis: verum

end;

assume ( dom the ResultSort of S = the carrier' of S & the carrier of S = {} & the carrier' of S <> {} ) ; :: according to INSTALG1:def 1 :: thesis: contradiction
hence contradiction ; :: thesis: verum