defpred S₁[ set ] means $1 in InputVertices IIG;
deffunc H₁( set ) -> set = s . $1;
deffunc H₂( Vertex of IIG) -> Element of Result (action_at $1),SCS = (Den (action_at $1),SCS) . ((action_at $1) depends_on_in s);
consider f being ManySortedSet of 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: dom f = the carrier of IIG by PARTFUN1:def 4;
A3: dom the Sorts of SCS = the carrier of IIG by PARTFUN1:def 4;
A4: InputVertices IIG misses InnerVertices IIG by XBOOLE_1:79;

now

let x be set ; :: 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 4;

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:5; :: thesis: verum

end;

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

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

end;

end;

end;

then reconsider f = f as State of SCS by A2, A3, 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) )
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 A4, XBOOLE_0:3;
hence f . v = (Den (action_at v),SCS) . ((action_at v) depends_on_in s) by A1; :: thesis: verum