theorem :: GLIB_010:116

for G1, G2 being _Graph
for F being PGraphMapping of G1,G2 holds
( F * (id G1) = F & (id G2) * F = F )