let o, m be set ; :: thesis: c1Cat* (o,m) is Category-like
set C = c1Cat* (o,m);
set CP = the Comp of (c1Cat* (o,m));
set CD = the Source of (c1Cat* (o,m));
set CC = the Target of (c1Cat* (o,m));
thus for f, g being Morphism of (c1Cat* (o,m)) holds
( [g,f] in dom the Comp of (c1Cat* (o,m)) iff dom g = cod f ) :: according to CAT_1:def 6 :: thesis: verum

proof

let f, g be Morphism of (c1Cat* (o,m)); :: thesis: ( [g,f] in dom the Comp of (c1Cat* (o,m)) iff dom g = cod f )
A1: dom the Comp of (c1Cat* (o,m)) = {[m,m]} by FUNCOP_1:13;
A2: ( f = m & g = m ) by TARSKI:def 1;
thus ( [g,f] in dom the Comp of (c1Cat* (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 (c1Cat* (o,m)) )
thus ( dom g = cod f implies [g,f] in dom the Comp of (c1Cat* (o,m)) ) by A1, A2, TARSKI:def 1; :: thesis: verum

end;