theorem Th12: :: FUNCTOR1:12

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 bijective & G is bijective holds
G * F is bijective by Th11, Th10;