theorem :: GLIBPRE0:97

for G1, G2 being non-Dmulti _Graph
for f being directed PVertexMapping of G1,G2
for v being Vertex of G1 st f is Disomorphism holds
( v .inDegree() = (f /. v) .inDegree() & v .outDegree() = (f /. v) .outDegree() )