set sc = Set-Constants SCS;

A1: dom (Set-Constants SCS) = SortsWithConstants 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

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

dom the Sorts of SCS = the carrier of IIG
by PARTFUN1:def 2;(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;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

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