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

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

let e be object ; :: thesis: ( e in (F _E) .: (v .edgesInOut()) implies b₁ in ((F _V) /. v) .edgesInOut() )
assume e in (F _E) .: (v .edgesInOut()) ; :: thesis: b₁ in ((F _V) /. v) .edgesInOut()
then consider e0 being object such that
A2: ( e0 in dom (F _E) & e0 in v .edgesInOut() & e = (F _E) . e0 ) by FUNCT_1:def 6;

per cases ( (the_Source_of G1) . e0 = v or (the_Target_of G1) . e0 = v ) by A2, GLIB_000:61;

suppose A3: (the_Source_of G1) . e0 = v ; :: thesis: b₁ in ((F _V) /. v) .edgesInOut()

set w = (the_Target_of G1) . e0;
A4: (the_Target_of G1) . e0 in dom (F _V) by A2, GLIB_010:5;
e0 Joins v,(the_Target_of G1) . e0,G1 by A2, A3, GLIB_000:def 13;
then (F _E) . e0 Joins (F _V) . v,(F _V) . ((the_Target_of G1) . e0),G2 by A1, A2, A4, GLIB_010:4;
then (F _E) . e0 Joins (F _V) /. v,(F _V) . ((the_Target_of G1) . e0),G2 by A1, PARTFUN1:def 6;
hence e in ((F _V) /. v) .edgesInOut() by A2, GLIB_000:62; :: thesis: verum

end;

suppose A5: (the_Target_of G1) . e0 = v ; :: thesis: b₁ in ((F _V) /. v) .edgesInOut()

set w = (the_Source_of G1) . e0;
A6: (the_Source_of G1) . e0 in dom (F _V) by A2, GLIB_010:5;
e0 Joins v,(the_Source_of G1) . e0,G1 by A2, A5, GLIB_000:def 13;
then (F _E) . e0 Joins (F _V) . v,(F _V) . ((the_Source_of G1) . e0),G2 by A1, A2, A6, GLIB_010:4;
then (F _E) . e0 Joins (F _V) /. v,(F _V) . ((the_Source_of G1) . e0),G2 by A1, PARTFUN1:def 6;
hence e in ((F _V) /. v) .edgesInOut() by A2, GLIB_000:62; :: thesis: verum

end;

end;

end;

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