theorem Th99: :: GLIBPRE0:93

for G1, G2 being _Graph
for F being PGraphMapping of G1,G2
for v being Vertex of G1 st F is isomorphism holds
v .degree() = ((F _V) /. v) .degree()