let G1, G2 be _Graph; :: thesis: for F being PGraphMapping of G1,G2
for v being Vertex of G1 st F is isomorphism holds
v .degree() = ((F _V) /. v) .degree()
let F0 be PGraphMapping of G1,G2; :: thesis: for v being Vertex of G1 st F0 is isomorphism holds
v .degree() = ((F0 _V) /. v) .degree()
let v be Vertex of G1; :: thesis: ( F0 is isomorphism implies v .degree() = ((F0 _V) /. v) .degree() )
assume A1: F0 is isomorphism ; :: thesis: v .degree() = ((F0 _V) /. v) .degree()
then F0 _E is one-to-one ;
then consider E being Subset of (the_Edges_of G2) such that
A2: for G3 being reverseEdgeDirections of G2,E ex F being PGraphMapping of G1,G3 st
( F = F0 & F is directed & ( F0 is weak_SG-embedding implies F is weak_SG-embedding ) & ( F0 is strong_SG-embedding implies F is strong_SG-embedding ) & ( F0 is isomorphism implies F is isomorphism ) ) by Th93;
set G3 = the reverseEdgeDirections of G2,E;
consider F being PGraphMapping of G1, the reverseEdgeDirections of G2,E such that
A3: ( F = F0 & F is directed ) and
( ( F0 is weak_SG-embedding implies F is weak_SG-embedding ) & ( F0 is strong_SG-embedding implies F is strong_SG-embedding ) ) and
A4: ( F0 is isomorphism implies F is isomorphism ) by A2;
( v .inDegree() = ((F _V) /. v) .inDegree() & v .outDegree() = ((F _V) /. v) .outDegree() ) by A1, A3, A4, Th98;
then A5: ((F _V) /. v) .degree() = v .degree() ;
( F0 is total & dom (F _V) = dom (F0 _V) & v in the_Vertices_of G1 ) by A1, A3;
then A6: ( v in dom (F0 _V) & v in dom (F _V) ) by GLIB_010:def 11;
(F0 _V) /. v = (F0 _V) . v by A6, PARTFUN1:def 6
.= (F _V) /. v by A3, A6, PARTFUN1:def 6 ;
hence v .degree() = ((F0 _V) /. v) .degree() by A5, Th60; :: thesis: verum