deffunc H₁( Vertex of IIG) -> Element of Result ((action_at $1),SCS) = (Den ((action_at $1),SCS)) . ((action_at $1) depends_on_in s);
deffunc H₂( set ) -> set = s . $1;
defpred S₁[ set ] means $1 in InputVertices IIG;
consider f being ManySortedSet of the carrier of IIG such that
A1: for v being Vertex of IIG st v in the carrier of IIG holds
( ( S₁[v] implies f . v = H₂(v) ) & ( not S₁[v] implies f . v = H₁(v) ) ) from PRE_CIRC:sch 2();

A2: now :: thesis: for x being object st x in dom the Sorts of SCS holds
f . x in the Sorts of SCS . x

let x be object ; :: thesis: ( x in dom the Sorts of SCS implies f . b₁ in the Sorts of SCS . b₁ )
assume x in dom the Sorts of SCS ; :: thesis: f . b₁ in the Sorts of SCS . b₁
then reconsider v = x as Vertex of IIG by PARTFUN1:def 2;

per cases ( v in InputVertices IIG or not v in InputVertices IIG ) ;

suppose v in InputVertices IIG ; :: thesis: f . b₁ in the Sorts of SCS . b₁

then f . v = s . v by A1;
hence f . x in the Sorts of SCS . x by CIRCUIT1:4; :: thesis: verum

end;

suppose A3: not v in InputVertices IIG ; :: thesis: f . b₁ in the Sorts of SCS . b₁

v in the carrier of IIG ;
then v in (InputVertices IIG) \/ (InnerVertices IIG) by XBOOLE_1:45;
then v in InnerVertices IIG by A3, XBOOLE_0:def 3;
then A4: the_result_sort_of (action_at v) = v by MSAFREE2:def 7;
f . x = (Den ((action_at v),SCS)) . ((action_at v) depends_on_in s) by A1, A3;
hence f . x in the Sorts of SCS . x by A4, CIRCUIT1:8; :: thesis: verum

end;

end;

end;

( dom f = the carrier of IIG & dom the Sorts of SCS = the carrier of IIG ) by PARTFUN1:def 2;
then reconsider f = f as State of SCS by A2, CARD_3:def 5;
take f ; :: thesis: for v being Vertex of IIG holds
( ( v in InputVertices IIG implies f . v = s . v ) & ( v in InnerVertices IIG implies f . v = (Den ((action_at v),SCS)) . ((action_at v) depends_on_in s) ) )
let v be Vertex of IIG; :: thesis: ( ( v in InputVertices IIG implies f . v = s . v ) & ( v in InnerVertices IIG implies f . v = (Den ((action_at v),SCS)) . ((action_at v) depends_on_in s) ) )
thus ( v in InputVertices IIG implies f . v = s . v ) by A1; :: thesis: ( v in InnerVertices IIG implies f . v = (Den ((action_at v),SCS)) . ((action_at v) depends_on_in s) )
A5: InputVertices IIG misses InnerVertices IIG by XBOOLE_1:79;
assume v in InnerVertices IIG ; :: thesis: f . v = (Den ((action_at v),SCS)) . ((action_at v) depends_on_in s)
then not v in InputVertices IIG by A5, XBOOLE_0:3;
hence f . v = (Den ((action_at v),SCS)) . ((action_at v) depends_on_in s) by A1; :: thesis: verum