let it1, it2 be State of SCS; :: thesis: ( ( for v being Vertex of IIG holds
( ( v in InputVertices IIG implies it1 . v = s . v ) & ( v in InnerVertices IIG implies it1 . v = (Den ((),SCS)) . () ) ) ) & ( for v being Vertex of IIG holds
( ( v in InputVertices IIG implies it2 . v = s . v ) & ( v in InnerVertices IIG implies it2 . v = (Den ((),SCS)) . () ) ) ) implies it1 = it2 )

assume that
A6: for v being Vertex of IIG holds
( ( v in InputVertices IIG implies it1 . v = s . v ) & ( v in InnerVertices IIG implies it1 . v = (Den ((),SCS)) . () ) ) and
A7: for v being Vertex of IIG holds
( ( v in InputVertices IIG implies it2 . v = s . v ) & ( v in InnerVertices IIG implies it2 . v = (Den ((),SCS)) . () ) ) ; :: thesis: it1 = it2
assume A8: it1 <> it2 ; :: thesis: contradiction
dom it2 = the carrier of IIG by CIRCUIT1:3;
then consider x being object such that
A9: x in dom it1 and
A10: it1 . x <> it2 . x by ;
reconsider v = x as Vertex of IIG by ;
A11: ( v in InnerVertices IIG implies it1 . v = (Den ((),SCS)) . () ) by A6;
dom it1 = the carrier of IIG by CIRCUIT1:3;
then v in () \/ () by ;
then A12: ( v in InputVertices IIG or v in InnerVertices IIG ) by XBOOLE_0:def 3;
( v in InputVertices IIG implies it1 . v = s . v ) by A6;
hence contradiction by A7, A10, A12, A11; :: thesis: verum