let f, g be Morphism of (1Cat (o,m)); :: according to CAT_1:def 6 :: thesis: ( [g,f] in dom the Comp of (1Cat (o,m)) iff dom g = cod f )
thus ( [g,f] in dom the Comp of (1Cat (o,m)) implies dom g = cod f ) by ZFMISC_1:def 10; :: thesis: ( dom g = cod f implies [g,f] in dom the Comp of (1Cat (o,m)) )
assume dom g = cod f ; :: thesis: [g,f] in dom the Comp of (1Cat (o,m))
A1: dom the Comp of (1Cat (o,m)) = {[m,m]} by FUNCOP_1:13;
( f = m & g = m ) by TARSKI:def 1;
hence [g,f] in dom the Comp of (1Cat (o,m)) by A1, TARSKI:def 1; :: thesis: verum