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