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-Dcontinuous & v in dom (F _V) holds
( (F _E) .: (v .edgesIn()) = ((F _V) /. v) .edgesIn() & (F _E) .: (v .edgesOut()) = ((F _V) /. v) .edgesOut() )
let F be PGraphMapping of G1,G2; :: thesis: for v being Vertex of G1 st F is onto & F is semi-Dcontinuous & v in dom (F _V) holds
( (F _E) .: (v .edgesIn()) = ((F _V) /. v) .edgesIn() & (F _E) .: (v .edgesOut()) = ((F _V) /. v) .edgesOut() )
let v be Vertex of G1; :: thesis: ( F is onto & F is semi-Dcontinuous & v in dom (F _V) implies ( (F _E) .: (v .edgesIn()) = ((F _V) /. v) .edgesIn() & (F _E) .: (v .edgesOut()) = ((F _V) /. v) .edgesOut() ) )
assume A1: ( F is onto & F is semi-Dcontinuous & v in dom (F _V) ) ; :: thesis: ( (F _E) .: (v .edgesIn()) = ((F _V) /. v) .edgesIn() & (F _E) .: (v .edgesOut()) = ((F _V) /. v) .edgesOut() )
then A2: ( (F _E) .: (v .edgesIn()) c= ((F _V) /. v) .edgesIn() & (F _E) .: (v .edgesOut()) c= ((F _V) /. v) .edgesOut() ) by Th87;

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

let e9 be object ; :: thesis: ( e9 in ((F _V) /. v) .edgesIn() implies e9 in (F _E) .: (v .edgesIn()) )
assume A3: e9 in ((F _V) /. v) .edgesIn() ; :: thesis: e9 in (F _E) .: (v .edgesIn())
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;
A5: (the_Target_of G2) . e9 = (F _V) /. v by A3, GLIB_000:56;
set w9 = (the_Source_of G2) . e9;
A6: (F _E) . e DJoins (the_Source_of G2) . e9,(F _V) /. v,G2 by A3, A4, A5, GLIB_000:def 14;
then (F _E) . e Joins (the_Source_of G2) . e9,(F _V) /. v,G2 by GLIB_000:16;
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
A7: ( w in dom (F _V) & (F _V) . w = (the_Source_of G2) . e9 ) by FUNCT_1:def 3;
(F _E) . e DJoins (F _V) . w,(F _V) . v,G2 by A1, A6, A7, PARTFUN1:def 6;
then A8: e DJoins w,v,G1 by A1, A4, A7, GLIB_010:def 17;
( e is set & w is set ) by TARSKI:1;
then e in v .edgesIn() by A8, GLIB_000:57;
hence e9 in (F _E) .: (v .edgesIn()) by A4, FUNCT_1:def 6; :: thesis: verum

end;

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

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

let e9 be object ; :: thesis: ( e9 in ((F _V) /. v) .edgesOut() implies e9 in (F _E) .: (v .edgesOut()) )
assume A9: e9 in ((F _V) /. v) .edgesOut() ; :: thesis: e9 in (F _E) .: (v .edgesOut())
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
A10: ( e in dom (F _E) & (F _E) . e = e9 ) by FUNCT_1:def 3;
A11: (the_Source_of G2) . e9 = (F _V) /. v by A9, GLIB_000:58;
set w9 = (the_Target_of G2) . e9;
A12: (F _E) . e DJoins (F _V) /. v,(the_Target_of G2) . e9,G2 by A9, A10, A11, GLIB_000:def 14;
then (F _E) . e Joins (F _V) /. v,(the_Target_of G2) . e9,G2 by GLIB_000:16;
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
A13: ( w in dom (F _V) & (F _V) . w = (the_Target_of G2) . e9 ) by FUNCT_1:def 3;
(F _E) . e DJoins (F _V) . v,(F _V) . w,G2 by A1, A12, A13, PARTFUN1:def 6;
then A14: e DJoins v,w,G1 by A1, A10, A13, GLIB_010:def 17;
( e is set & w is set ) by TARSKI:1;
then e in v .edgesOut() by A14, GLIB_000:59;
hence e9 in (F _E) .: (v .edgesOut()) by A10, FUNCT_1:def 6; :: thesis: verum

end;

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