for C, D, E being Category
for F being Functor of C,E
for G being Functor of D,E
for k being Element of commaMorphs (F,G) st ex c being Object of C ex d being Object of D ex f being Morphism of E st f in Hom ((F . c),(G . d)) holds
( k = [[(k `11),(k `12)],[(k `21),(k `22)]] & dom (k `21) = (k `11) `11 & cod (k `21) = (k `12) `11 & dom (k `22) = (k `11) `12 & cod (k `22) = (k `12) `12 & ((k `12) `2) (*) (F . (k `21)) = (G . (k `22)) (*) ((k `11) `2) )