theorem :: GLIB_010:91

for G1, G2 being _Graph
for F being non empty one-to-one PGraphMapping of G1,G2 holds card ((dom F) .loops()) = card ((rng F) .loops())