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:72;
A4:
cod (F . (k1 `21)) = F . (cod (k1 `21))
by CAT_1:72;
A5:
cod ((k1 `12) `2) = G . ((k1 `12) `12)
by A1, Th1;
A6:
dom (k1 `22) = (k1 `11) `12
by A1, Th2;
A7:
( ((k2 `12) `2) (*) (F . (k2 `21)) = (G . (k2 `22)) (*) ((k2 `11) `2) & dom ((k2 `12) `2) = F . ((k2 `12) `11) )
by A1, Th1, Th2;
A8:
cod (G . (k1 `22)) = G . (cod (k1 `22))
by CAT_1:72;
A9:
( ((k1 `12) `2) (*) (F . (k1 `21)) = (G . (k1 `22)) (*) ((k1 `11) `2) & dom ((k1 `12) `2) = F . ((k1 `12) `11) )
by A1, Th1, Th2;
A10:
dom (G . (k2 `22)) = G . (dom (k2 `22))
by CAT_1:72;
A11:
( cod ((k1 `11) `2) = G . ((k1 `11) `12) & dom (G . (k1 `22)) = G . (dom (k1 `22)) )
by A1, Th1, CAT_1:72;
A12:
cod (k2 `21) = (k2 `12) `11
by A1, Th2;
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, Def2;
A14:
dom (k2 `22) = (k2 `11) `12
by A1, Th2;
A15:
cod (k1 `22) = (k1 `12) `12
by A1, Th2;
then A16:
( dom ((k2 `22) (*) (k1 `22)) = dom (k1 `22) & cod ((k2 `22) (*) (k1 `22)) = cod (k2 `22) )
by A2, A14, CAT_1:17;
A17:
( dom (k1 `21) = (k1 `11) `11 & cod (k2 `22) = (k2 `12) `12 )
by A1, Th2;
A18:
cod (k1 `21) = (k1 `12) `11
by A1, Th2;
A19:
dom (k2 `21) = (k2 `11) `11
by A1, Th2;
then A20:
( dom ((k2 `21) (*) (k1 `21)) = dom (k1 `21) & cod ((k2 `21) (*) (k1 `21)) = cod (k2 `21) )
by A2, A18, CAT_1:17;
((k2 `12) `2) (*) (F . ((k2 `21) (*) (k1 `21))) =
((k2 `12) `2) (*) ((F . (k2 `21)) (*) (F . (k1 `21)))
by A2, A18, A19, CAT_1:64
.=
((G . (k2 `22)) (*) ((k2 `11) `2)) (*) (F . (k1 `21))
by A2, A18, A19, A12, A7, A3, A4, CAT_1:18
.=
(G . (k2 `22)) (*) ((G . (k1 `22)) (*) ((k1 `11) `2))
by A2, A18, A14, A9, A5, A4, A10, CAT_1:18
.=
((G . (k2 `22)) (*) (G . (k1 `22))) (*) ((k1 `11) `2)
by A2, A6, A15, A14, A10, A11, A8, CAT_1:18
.=
(G . ((k2 `22) (*) (k1 `22))) (*) ((k1 `11) `2)
by A2, A15, A14, CAT_1:64
;
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