let C, D, E be Category; :: thesis: 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) )
let F be Functor of C,E; :: thesis: 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) )
let G be Functor of D,E; :: thesis: 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) )
let o be Element of commaObjs (F,G); :: thesis: ( 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)) implies ( 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) ) )
assume 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)) ; :: thesis: ( 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) )
then A1: commaObjs (F,G) = { [[c,d],f] where c is Object of C, d is Object of D, f is Morphism of E : f in Hom ((F . c),(G . d)) } by Def1;
o in commaObjs (F,G) ;
then consider c being Object of C, d being Object of D, f being Morphism of E such that
A2: o = [[c,d],f] and
A3: f in Hom ((F . c),(G . d)) by A1;
( o `11 = c & o `12 = d ) by A2, MCART_1:85;
hence ( 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) ) by A2, A3, CAT_1:1; :: thesis: verum