theorem :: GLIB_010:107
for G1, G2, G3 being _Graph
for F1 being PGraphMapping of G1,G2
for F2 being PGraphMapping of G2,G3 st F1 is weak_SG-embedding & F2 is weak_SG-embedding holds
F2 * F1 is weak_SG-embedding by Th104;