let G be non empty void ManySortedSign ; :: thesis: InputVertices G = the carrier of G
dom the ResultSort of G = the carrier' of G by FUNCT_2:def 1
.= {} ;
then rng the ResultSort of G = {} by RELAT_1:65;
hence InputVertices G = the carrier of G ; :: thesis: verum