deffunc H1( Vertex of IIG) -> Element of Result ((),SCS) = (Den ((),SCS)) . (() depends_on_in s);
deffunc H2( set ) -> set = s . \$1;
defpred S1[ 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
( ( S1[v] implies f . v = H2(v) ) & ( not S1[v] implies f . v = H1(v) ) ) from
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 . b1 in the Sorts of SCS . b1 )
assume x in dom the Sorts of SCS ; :: thesis: f . b1 in the Sorts of SCS . b1
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 . b1 in the Sorts of SCS . b1
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 . b1 in the Sorts of SCS . b1
v in the carrier of IIG ;
then v in () \/ () by XBOOLE_1:45;
then v in InnerVertices IIG by ;
then A4: the_result_sort_of () = v by MSAFREE2:def 7;
f . x = (Den ((),SCS)) . () by A1, A3;
hence f . x in the Sorts of SCS . x by ; :: 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 ;
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 ((),SCS)) . () ) )

let v be Vertex of IIG; :: thesis: ( ( v in InputVertices IIG implies f . v = s . v ) & ( v in InnerVertices IIG implies f . v = (Den ((),SCS)) . () ) )
thus ( v in InputVertices IIG implies f . v = s . v ) by A1; :: thesis: ( v in InnerVertices IIG implies f . v = (Den ((),SCS)) . () )
A5: InputVertices IIG misses InnerVertices IIG by XBOOLE_1:79;
assume v in InnerVertices IIG ; :: thesis: f . v = (Den ((),SCS)) . ()
then not v in InputVertices IIG by ;
hence f . v = (Den ((),SCS)) . () by A1; :: thesis: verum