let it1, it2 be State of SCS; ( ( 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) ) )
; it1 = it2
assume A8:
it1 <> it2
; 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; verum