set k22 = (k2 `22 ) * (k1 `22 );
set k21 = (k2 `21 ) * (k1 `21 );
A3:
( F . (cod (k2 `21 )) = cod (F . (k2 `21 )) & dom (F . (k2 `21 )) = F . (dom (k2 `21 )) )
by CAT_1:109;
A4:
cod (F . (k1 `21 )) = F . (cod (k1 `21 ))
by CAT_1:109;
A5:
cod ((k1 `12 ) `2 ) = G . ((k1 `12 ) `12 )
by A1, Th2;
A6:
dom (k1 `22 ) = (k1 `11 ) `12
by A1, Th3;
A7:
( ((k2 `12 ) `2 ) * (F . (k2 `21 )) = (G . (k2 `22 )) * ((k2 `11 ) `2 ) & dom ((k2 `12 ) `2 ) = F . ((k2 `12 ) `11 ) )
by A1, Th2, Th3;
A8:
cod (G . (k1 `22 )) = G . (cod (k1 `22 ))
by CAT_1:109;
A9:
( ((k1 `12 ) `2 ) * (F . (k1 `21 )) = (G . (k1 `22 )) * ((k1 `11 ) `2 ) & dom ((k1 `12 ) `2 ) = F . ((k1 `12 ) `11 ) )
by A1, Th2, Th3;
A10:
dom (G . (k2 `22 )) = G . (dom (k2 `22 ))
by CAT_1:109;
A11:
( cod ((k1 `11 ) `2 ) = G . ((k1 `11 ) `12 ) & dom (G . (k1 `22 )) = G . (dom (k1 `22 )) )
by A1, Th2, CAT_1:109;
A12:
cod (k2 `21 ) = (k2 `12 ) `11
by A1, Th3;
A13:
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 A1, Def6;
A14:
dom (k2 `22 ) = (k2 `11 ) `12
by A1, Th3;
A15:
cod (k1 `22 ) = (k1 `12 ) `12
by A1, Th3;
then A16:
( dom ((k2 `22 ) * (k1 `22 )) = dom (k1 `22 ) & cod ((k2 `22 ) * (k1 `22 )) = cod (k2 `22 ) )
by A2, A14, CAT_1:42;
A17:
( dom (k1 `21 ) = (k1 `11 ) `11 & cod (k2 `22 ) = (k2 `12 ) `12 )
by A1, Th3;
A18:
cod (k1 `21 ) = (k1 `12 ) `11
by A1, Th3;
A19:
dom (k2 `21 ) = (k2 `11 ) `11
by A1, Th3;
then A20:
( dom ((k2 `21 ) * (k1 `21 )) = dom (k1 `21 ) & cod ((k2 `21 ) * (k1 `21 )) = cod (k2 `21 ) )
by A2, A18, CAT_1:42;
((k2 `12 ) `2 ) * (F . ((k2 `21 ) * (k1 `21 ))) =
((k2 `12 ) `2 ) * ((F . (k2 `21 )) * (F . (k1 `21 )))
by A2, A18, A19, CAT_1:99
.=
((G . (k2 `22 )) * ((k2 `11 ) `2 )) * (F . (k1 `21 ))
by A2, A18, A19, A12, A7, A3, A4, CAT_1:43
.=
(G . (k2 `22 )) * ((G . (k1 `22 )) * ((k1 `11 ) `2 ))
by A2, A18, A14, A9, A5, A4, A10, CAT_1:43
.=
((G . (k2 `22 )) * (G . (k1 `22 ))) * ((k1 `11 ) `2 )
by A2, A6, A15, A14, A10, A11, A8, CAT_1:43
.=
(G . ((k2 `22 ) * (k1 `22 ))) * ((k1 `11 ) `2 )
by A2, A15, A14, CAT_1:99
;
then
[[(k1 `11 ),(k2 `12 )],[((k2 `21 ) * (k1 `21 )),((k2 `22 ) * (k1 `22 ))]] in commaMorphs F,G
by A6, A12, A17, A13, A20, A16;
hence
[[(k1 `11 ),(k2 `12 )],[((k2 `21 ) * (k1 `21 )),((k2 `22 ) * (k1 `22 ))]] is Element of commaMorphs F,G
; verum