let o, m be set ; :: thesis:
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));
set CI = the Id 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 the Source of (c1Cat (o,m)) . g = the Target of (c1Cat (o,m)) . f ) :: according to CAT_1:def 5 :: thesis:

let f, g be Morphism of (c1Cat (o,m)); :: thesis:
A1: dom the Comp of (c1Cat (o,m)) = {[m,m]} by FUNCOP_1:13;
( f = m & g = m ) by TARSKI:def 1;
hence ( [g,f] in dom the Comp of (c1Cat (o,m)) iff the Source of (c1Cat (o,m)) . g = the Target of (c1Cat (o,m)) . f ) by A1, TARSKI:def 1; :: thesis:

end;

thus for f, g being Morphism of (c1Cat (o,m)) st the Source of (c1Cat (o,m)) . g = the Target of (c1Cat (o,m)) . f holds
( the Source of (c1Cat (o,m)) . ( the Comp of (c1Cat (o,m)) . (g,f)) = the Source of (c1Cat (o,m)) . f & the Target of (c1Cat (o,m)) . ( the Comp of (c1Cat (o,m)) . (g,f)) = the Target of (c1Cat (o,m)) . g ) :: thesis:

let f, g be Morphism of (c1Cat (o,m)); :: thesis:
the Comp of (c1Cat (o,m)) . (g,f) = m by FUNCOP_1:77;
then reconsider gf = the Comp of (c1Cat (o,m)) . (g,f) as Morphism of (c1Cat (o,m)) by TARSKI:def 1;
the Source of (c1Cat (o,m)) . gf = o by FUNCT_2:50;
hence ( the Source of (c1Cat (o,m)) . g = the Target of (c1Cat (o,m)) . f implies ( the Source of (c1Cat (o,m)) . ( the Comp of (c1Cat (o,m)) . (g,f)) = the Source of (c1Cat (o,m)) . f & the Target of (c1Cat (o,m)) . ( the Comp of (c1Cat (o,m)) . (g,f)) = the Target of (c1Cat (o,m)) . g ) ) by FUNCT_2:50; :: thesis:

end;

thus for f, g, h being Morphism of (c1Cat (o,m)) st the Source of (c1Cat (o,m)) . h = the Target of (c1Cat (o,m)) . g & the Source of (c1Cat (o,m)) . g = the Target of (c1Cat (o,m)) . f holds
the Comp of (c1Cat (o,m)) . (h,( the Comp of (c1Cat (o,m)) . (g,f))) = the Comp of (c1Cat (o,m)) . (( the Comp of (c1Cat (o,m)) . (h,g)),f) :: thesis:

let f, g, h be Morphism of (c1Cat (o,m)); :: thesis:
( the Comp of (c1Cat (o,m)) . (g,f) = m & the Comp of (c1Cat (o,m)) . (h,g) = m ) by FUNCOP_1:77;
then reconsider gf = the Comp of (c1Cat (o,m)) . (g,f), hg = the Comp of (c1Cat (o,m)) . (h,g) as Morphism of (c1Cat (o,m)) by TARSKI:def 1;
( the Comp of (c1Cat (o,m)) . (h,gf) = m & the Comp of (c1Cat (o,m)) . (hg,f) = m ) by FUNCOP_1:77;
hence ( the Source of (c1Cat (o,m)) . h = the Target of (c1Cat (o,m)) . g & the Source of (c1Cat (o,m)) . g = the Target of (c1Cat (o,m)) . f implies the Comp of (c1Cat (o,m)) . (h,( the Comp of (c1Cat (o,m)) . (g,f))) = the Comp of (c1Cat (o,m)) . (( the Comp of (c1Cat (o,m)) . (h,g)),f) ) ; :: thesis:

end;

let b be Object of (c1Cat (o,m)); :: thesis:
b = o by TARSKI:def 1;
hence ( the Source of (c1Cat (o,m)) . ( the Id of (c1Cat (o,m)) . b) = b & the Target of (c1Cat (o,m)) . ( the Id of (c1Cat (o,m)) . b) = b ) by FUNCT_2:50; :: thesis:
thus for f being Morphism of (c1Cat (o,m)) st the Target of (c1Cat (o,m)) . f = b holds
the Comp of (c1Cat (o,m)) . (( the Id of (c1Cat (o,m)) . b),f) = f :: thesis:

let f be Morphism of (c1Cat (o,m)); :: thesis:
f = m by TARSKI:def 1;
hence ( the Target of (c1Cat (o,m)) . f = b implies the Comp of (c1Cat (o,m)) . (( the Id of (c1Cat (o,m)) . b),f) = f ) by FUNCOP_1:77; :: thesis:

end;

let g be Morphism of (c1Cat (o,m)); :: thesis:
assume the Source of (c1Cat (o,m)) . g = b ; :: thesis:
g = m by TARSKI:def 1;
hence the Comp of (c1Cat (o,m)) . (g,( the Id of (c1Cat (o,m)) . b)) = g by FUNCOP_1:77; :: thesis: