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

( ( 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