let C, D, E be Category; :: thesis: 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 ) )
let F be Functor of C,E; :: thesis: 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 ) )
let G be Functor of D,E; :: thesis: 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 ) )
let k be Element of commaMorphs 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 ( 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 ) ) )
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: ( 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 ) )
then A1: commaMorphs F,G = { [[o1,o2],[g,h]] where g is Morphism of C, h is Morphism of D, o1, o2 is Element of commaObjs F,G : ( dom g = o1 `11 & cod g = o2 `11 & dom h = o1 `12 & cod h = o2 `12 & (o2 `2 ) * (F . g) = (G . h) * (o1 `2 ) ) } by Def6;
k in commaMorphs F,G ;
then consider g being Morphism of C, h being Morphism of D, o1, o2 being Element of commaObjs F,G such that
A2: k = [[o1,o2],[g,h]] and
A3: ( dom g = o1 `11 & cod g = o2 `11 & dom h = o1 `12 & cod h = o2 `12 & (o2 `2 ) * (F . g) = (G . h) * (o1 `2 ) ) by A1;
A4: k `21 = g by A2, MCART_1:89;
( k `11 = o1 & k `12 = o2 ) by A2, MCART_1:89;
hence ( 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 ) ) by A2, A3, A4, MCART_1:89; :: thesis: verum