theorem :: GLIBPRE0:98

for G1, G2 being non-multi _Graph
for f being PVertexMapping of G1,G2
for v being Vertex of G1 st f is isomorphism holds
v .degree() = (f /. v) .degree()