let G1, G2 be _Graph; :: thesis: for F being PGraphMapping of G1,G2
for v being Vertex of G1 st F is Disomorphism 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 Disomorphism 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 Disomorphism implies ( (F _E) .: (v .edgesIn()) = ((F _V) /. v) .edgesIn() & (F _E) .: (v .edgesOut()) = ((F _V) /. v) .edgesOut() ) )
assume A1: F is Disomorphism ; :: thesis: ( (F _E) .: (v .edgesIn()) = ((F _V) /. v) .edgesIn() & (F _E) .: (v .edgesOut()) = ((F _V) /. v) .edgesOut() )
then dom (F _V) = the_Vertices_of G1 by GLIB_010:def 11;
hence ( (F _E) .: (v .edgesIn()) = ((F _V) /. v) .edgesIn() & (F _E) .: (v .edgesOut()) = ((F _V) /. v) .edgesOut() ) by A1, Th89; :: thesis: verum