theorem :: GLIB_010:100

for G1, G2, G3 being _Graph
for F1 being PGraphMapping of G1,G2
for F2 being PGraphMapping of G2,G3 holds
( (F2 * F1) _V = (F2 _V) * (F1 _V) & (F2 * F1) _E = (F2 _E) * (F1 _E) ) ;