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