let C, D, E be 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) )
let F be 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 G be 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 k be Element of commaMorphs (F,G); ( 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))
; ( 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 Def2;
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:85;
( k `11 = o1 & k `12 = o2 )
by A2, MCART_1:85;
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:85; verum