A1: dom iv = InputVertices IIG by PARTFUN1:def 2;
then ( dom the Sorts of SCS = the carrier of IIG & ( for x being set st x in dom iv holds
iv . x in the Sorts of SCS . x ) ) by MSAFREE2:def 5, PARTFUN1:def 2;
hence s +* iv is State of SCS by A1, PRE_CIRC:6; :: thesis: verum