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