theorem Th1: :: COMMACAT:1

for C, D, E being Category
for F being Functor of C,E
for G being Functor of D,E
for o being Element of commaObjs (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
( o = [[(o `11),(o `12)],(o `2)] & o `2 in Hom ((F . (o `11)),(G . (o `12))) & dom (o `2) = F . (o `11) & cod (o `2) = G . (o `12) )