let G1, G2 be _Graph; :: thesis: for F being PGraphMapping of G1,G2
for v being Vertex of G1 st F is directed & v in dom (F _V) holds
( (F _E) .: (v .edgesIn()) c= ((F _V) /. v) .edgesIn() & (F _E) .: (v .edgesOut()) c= ((F _V) /. v) .edgesOut() )
let F be PGraphMapping of G1,G2; :: thesis: for v being Vertex of G1 st F is directed & v in dom (F _V) holds
( (F _E) .: (v .edgesIn()) c= ((F _V) /. v) .edgesIn() & (F _E) .: (v .edgesOut()) c= ((F _V) /. v) .edgesOut() )
let v be Vertex of G1; :: thesis: ( F is directed & v in dom (F _V) implies ( (F _E) .: (v .edgesIn()) c= ((F _V) /. v) .edgesIn() & (F _E) .: (v .edgesOut()) c= ((F _V) /. v) .edgesOut() ) )
assume A1: ( F is directed & v in dom (F _V) ) ; :: thesis: ( (F _E) .: (v .edgesIn()) c= ((F _V) /. v) .edgesIn() & (F _E) .: (v .edgesOut()) c= ((F _V) /. v) .edgesOut() )

now :: thesis: for e being object st e in (F _E) .: (v .edgesIn()) holds
e in ((F _V) /. v) .edgesIn()

let e be object ; :: thesis: ( e in (F _E) .: (v .edgesIn()) implies e in ((F _V) /. v) .edgesIn() )
assume e in (F _E) .: (v .edgesIn()) ; :: thesis: e in ((F _V) /. v) .edgesIn()
then consider e0 being object such that
A2: ( e0 in dom (F _E) & e0 in v .edgesIn() & e = (F _E) . e0 ) by FUNCT_1:def 6;
A3: (the_Target_of G1) . e0 = v by A2, GLIB_000:56;
set w = (the_Source_of G1) . e0;
A4: (the_Source_of G1) . e0 in dom (F _V) by A2, GLIB_010:5;
e0 DJoins (the_Source_of G1) . e0,v,G1 by A2, A3, GLIB_000:def 14;
then (F _E) . e0 DJoins (F _V) . ((the_Source_of G1) . e0),(F _V) . v,G2 by A1, A2, A4, GLIB_010:def 14;
then (F _E) . e0 DJoins (F _V) . ((the_Source_of G1) . e0),(F _V) /. v,G2 by A1, PARTFUN1:def 6;
hence e in ((F _V) /. v) .edgesIn() by A2, GLIB_000:57; :: thesis: verum

end;

hence (F _E) .: (v .edgesIn()) c= ((F _V) /. v) .edgesIn() by TARSKI:def 3; :: thesis: (F _E) .: (v .edgesOut()) c= ((F _V) /. v) .edgesOut()

now :: thesis: for e being object st e in (F _E) .: (v .edgesOut()) holds
e in ((F _V) /. v) .edgesOut()

let e be object ; :: thesis: ( e in (F _E) .: (v .edgesOut()) implies e in ((F _V) /. v) .edgesOut() )
assume e in (F _E) .: (v .edgesOut()) ; :: thesis: e in ((F _V) /. v) .edgesOut()
then consider e0 being object such that
A5: ( e0 in dom (F _E) & e0 in v .edgesOut() & e = (F _E) . e0 ) by FUNCT_1:def 6;
A6: (the_Source_of G1) . e0 = v by A5, GLIB_000:58;
set w = (the_Target_of G1) . e0;
A7: (the_Target_of G1) . e0 in dom (F _V) by A5, GLIB_010:5;
e0 DJoins v,(the_Target_of G1) . e0,G1 by A5, A6, GLIB_000:def 14;
then (F _E) . e0 DJoins (F _V) . v,(F _V) . ((the_Target_of G1) . e0),G2 by A1, A5, A7, GLIB_010:def 14;
then (F _E) . e0 DJoins (F _V) /. v,(F _V) . ((the_Target_of G1) . e0),G2 by A1, PARTFUN1:def 6;
hence e in ((F _V) /. v) .edgesOut() by A5, GLIB_000:59; :: thesis: verum

end;

hence (F _E) .: (v .edgesOut()) c= ((F _V) /. v) .edgesOut() by TARSKI:def 3; :: thesis: verum