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 ((action_at v),SCS)) . ((action_at v) depends_on_in s) ) ) ) & ( for v being Vertex of IIG holds
( ( v in InputVertices IIG implies it2 . v = s . v ) & ( v in InnerVertices IIG implies it2 . v = (Den ((action_at v),SCS)) . ((action_at v) depends_on_in s) ) ) ) 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 ((action_at v),SCS)) . ((action_at v) depends_on_in s) ) ) 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 ((action_at v),SCS)) . ((action_at v) depends_on_in s) ) ) ; :: 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 A8, CIRCUIT1:3, FUNCT_1:2;
reconsider v = x as Vertex of IIG by A9, CIRCUIT1:3;
A11: ( v in InnerVertices IIG implies it1 . v = (Den ((action_at v),SCS)) . ((action_at v) depends_on_in s) ) by A6;
dom it1 = the carrier of IIG by CIRCUIT1:3;
then v in (InputVertices IIG) \/ (InnerVertices IIG) by A9, XBOOLE_1:45;
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