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

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