theorem Th6: :: FUNCTOR1:6

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 one-to-one & G is one-to-one holds
G * F is one-to-one