theorem Th10: :: FUNCTOR1:10

for C1 being non empty AltGraph
for C2, C3 being non empty reflexive AltGraph
for F being feasible FunctorStr over C1,C2
for G being FunctorStr over C2,C3 st F is injective & G is injective holds
G * F is injective by Th7, Th6;