let o, m be set ; 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 )
CAT_1:def 6 verum