:: deftheorem defines comp-preserving FUNCTOR0:def 21 :
for C1, C2 being non empty AltCatStr
for F being FunctorStr over C1,C2 holds
( F is comp-preserving iff for o1, o2, o3 being Object of C1 st <^o1,o2^> <> {} & <^o2,o3^> <> {} holds
for f being Morphism of o1,o2
for g being Morphism of o2,o3 ex f9 being Morphism of (F . o1),(F . o2) ex g9 being Morphism of (F . o2),(F . o3) st
( f9 = (Morph-Map (F,o1,o2)) . f & g9 = (Morph-Map (F,o2,o3)) . g & (Morph-Map (F,o1,o3)) . (g * f) = g9 * f9 ) );