theorem Th30: :: CATALG_1:30

for C1, C2 being Category
for F being Functor of C1,C2
for a, b, c being Object of C1
for f, g being Morphism of C1 st f in Hom (a,b) & g in Hom (b,c) holds
for x being Element of Args ((compsym (a,b,c)),(MSAlg C1)) st x = <*g,f*> holds
for H being ManySortedFunction of (MSAlg C1),((MSAlg C2) | ((CatSign the carrier of C1),(Upsilon F),(Psi F))) st H = F -MSF ( the carrier of (CatSign the carrier of C1), the Sorts of (MSAlg C1)) holds
H # x = <*(F . g),(F . f)*>