set sc = Set-Constants SCS;
A1: dom (Set-Constants SCS) = SortsWithConstants IIG by PARTFUN1:def 2;

A2: now :: thesis: for x being set st x in dom (Set-Constants SCS) holds
(Set-Constants SCS) . x in the Sorts of SCS . x

let x be set ; :: thesis: ( x in dom (Set-Constants SCS) implies (Set-Constants SCS) . x in the Sorts of SCS . x )
assume A3: 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 A3, CIRCUIT1:def 1;
hence (Set-Constants SCS) . x in the Sorts of SCS . x ; :: thesis: verum

end;

dom the Sorts of SCS = the carrier of IIG by PARTFUN1:def 2;
hence (s +* (0 -th_InputValues InpFs)) +* (Set-Constants SCS) is State of SCS by A1, A2, PRE_CIRC:6; :: thesis: verum