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 Def5;
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;
A4: o `2 = f by A2, MCART_1:7;
( o `11 = c & o `12 = d ) by A2, MCART_1:89;
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, A4, CAT_1:18; :: thesis: verum