let G1, G2 be _Graph; :: thesis: for F being PGraphMapping of G1,G2
for v being Vertex of G1 st F is onto & F is semi-continuous & v in dom (F _V) holds
(F _E) .: (v .edgesInOut()) = ((F _V) /. v) .edgesInOut()
let F be PGraphMapping of G1,G2; :: thesis: for v being Vertex of G1 st F is onto & F is semi-continuous & v in dom (F _V) holds
(F _E) .: (v .edgesInOut()) = ((F _V) /. v) .edgesInOut()
let v be Vertex of G1; :: thesis: ( F is onto & F is semi-continuous & v in dom (F _V) implies (F _E) .: (v .edgesInOut()) = ((F _V) /. v) .edgesInOut() )
assume A1: ( F is onto & F is semi-continuous & v in dom (F _V) ) ; :: thesis: (F _E) .: (v .edgesInOut()) = ((F _V) /. v) .edgesInOut()
then A2: (F _E) .: (v .edgesInOut()) c= ((F _V) /. v) .edgesInOut() by Th86;

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

let e9 be object ; :: thesis: ( e9 in ((F _V) /. v) .edgesInOut() implies b₁ in (F _E) .: (v .edgesInOut()) )
assume A3: e9 in ((F _V) /. v) .edgesInOut() ; :: thesis: b₁ in (F _E) .: (v .edgesInOut())
then e9 in the_Edges_of G2 ;
then e9 in rng (F _E) by A1, GLIB_010:def 12;
then consider e being object such that
A4: ( e in dom (F _E) & (F _E) . e = e9 ) by FUNCT_1:def 3;

per cases ( (the_Source_of G2) . e9 = (F _V) /. v or (the_Target_of G2) . e9 = (F _V) /. v ) by A3, GLIB_000:61;

suppose A5: (the_Source_of G2) . e9 = (F _V) /. v ; :: thesis: b₁ in (F _E) .: (v .edgesInOut())

set w9 = (the_Target_of G2) . e9;
A6: (F _E) . e Joins (F _V) /. v,(the_Target_of G2) . e9,G2 by A3, A4, A5, GLIB_000:def 13;
then (the_Target_of G2) . e9 in the_Vertices_of G2 by GLIB_000:13;
then (the_Target_of G2) . e9 in rng (F _V) by A1, GLIB_010:def 12;
then consider w being object such that
A7: ( w in dom (F _V) & (F _V) . w = (the_Target_of G2) . e9 ) by FUNCT_1:def 3;
(F _E) . e Joins (F _V) . v,(F _V) . w,G2 by A1, A6, A7, PARTFUN1:def 6;
then e in v .edgesInOut() by A1, A4, A7, GLIB_010:def 15, GLIB_000:62;
hence e9 in (F _E) .: (v .edgesInOut()) by A4, FUNCT_1:def 6; :: thesis: verum

end;

suppose A8: (the_Target_of G2) . e9 = (F _V) /. v ; :: thesis: b₁ in (F _E) .: (v .edgesInOut())

set w9 = (the_Source_of G2) . e9;
A9: (F _E) . e Joins (F _V) /. v,(the_Source_of G2) . e9,G2 by A3, A4, A8, GLIB_000:def 13;
then (the_Source_of G2) . e9 in the_Vertices_of G2 by GLIB_000:13;
then (the_Source_of G2) . e9 in rng (F _V) by A1, GLIB_010:def 12;
then consider w being object such that
A10: ( w in dom (F _V) & (F _V) . w = (the_Source_of G2) . e9 ) by FUNCT_1:def 3;
(F _E) . e Joins (F _V) . v,(F _V) . w,G2 by A1, A9, A10, PARTFUN1:def 6;
then e in v .edgesInOut() by A1, A4, A10, GLIB_010:def 15, GLIB_000:62;
hence e9 in (F _E) .: (v .edgesInOut()) by A4, FUNCT_1:def 6; :: thesis: verum

end;

end;

end;

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