let G1, G2 be _Graph; :: thesis: for F being PGraphMapping of G1,G2
for v being Vertex of G1 st F is Disomorphism holds
( v .inDegree() = ((F _V) /. v) .inDegree() & v .outDegree() = ((F _V) /. v) .outDegree() )
let F be PGraphMapping of G1,G2; :: thesis: for v being Vertex of G1 st F is Disomorphism holds
( v .inDegree() = ((F _V) /. v) .inDegree() & v .outDegree() = ((F _V) /. v) .outDegree() )
let v be Vertex of G1; :: thesis: ( F is Disomorphism implies ( v .inDegree() = ((F _V) /. v) .inDegree() & v .outDegree() = ((F _V) /. v) .outDegree() ) )
assume A1: F is Disomorphism ; :: thesis: ( v .inDegree() = ((F _V) /. v) .inDegree() & v .outDegree() = ((F _V) /. v) .outDegree() )
then dom (F _V) = the_Vertices_of G1 by GLIB_010:def 11;
then A2: ( ((F _V) /. v) .inDegree() c= v .inDegree() & ((F _V) /. v) .outDegree() c= v .outDegree() ) by A1, Th96;
( v .inDegree() c= ((F _V) /. v) .inDegree() & v .outDegree() c= ((F _V) /. v) .outDegree() ) by A1, Th94;
hence ( v .inDegree() = ((F _V) /. v) .inDegree() & v .outDegree() = ((F _V) /. v) .outDegree() ) by A2, XBOOLE_0:def 10; :: thesis: verum