set sc = Set-Constants SCS;
A1: ( dom (Set-Constants SCS) = SortsWithConstants IIG & dom the Sorts of SCS = the carrier of IIG ) by PARTFUN1:def 4;

now

let x be set ; :: thesis: ( x in dom (Set-Constants SCS) implies (Set-Constants SCS) . x in the Sorts of SCS . x )
assume A2: x in dom (Set-Constants SCS) ; :: thesis: (Set-Constants SCS) . x in the Sorts of SCS . x
then reconsider v = x as Vertex of IIG by A1;
(Set-Constants SCS) . x in Constants SCS,v by A2, CIRCUIT1:def 1;
hence (Set-Constants SCS) . x in the Sorts of SCS . x ; :: thesis: verum

end;

hence (s +* (0 -th_InputValues InpFs)) +* (Set-Constants SCS) is State of SCS by A1, PRE_CIRC:9; :: thesis: verum