let X be set ; :: thesis:
let a be Element of (CohCat X); :: thesis:
let aa be Element of CSp X; :: thesis:
assume A1: a = aa ; :: thesis:
let i be Morphism of a,a; :: thesis:
assume A2: i = id$ aa ; :: thesis:
let b be Element of (CohCat X); :: thesis:
thus ( Hom (a,b) <> {} implies for g being Morphism of a,b holds g (*) i = g ) :: thesis:

proof

assume A3: Hom (a,b) <> {} ; :: thesis:
let g be Morphism of a,b; :: thesis:
reconsider gg = g as Element of MapsC X ;
Hom (a,a) <> {} ;
then A4: cod i = a by CAT_1:5
.= dom g by A3, CAT_1:5 ;
A5: dom gg = dom g by Def11
.= aa by A1, A3, CAT_1:5 ;
then A6: cod (id$ aa) = dom gg ;
[g,i] in dom the Comp of (CohCat X) by A4, CAT_1:def 6;
hence g (*) i = the Comp of (CohCat X) . (g,i) by CAT_1:def 1
.= gg * (id$ aa) by A6, A2, Def13
.= g by A5, Th25 ;
:: thesis:

end;

thus ( Hom (b,a) <> {} implies for f being Morphism of b,a holds i (*) f = f ) :: thesis:

proof

assume A7: Hom (b,a) <> {} ; :: thesis:
let g be Morphism of b,a; :: thesis:
reconsider gg = g as Element of MapsC X ;
Hom (a,a) <> {} ;
then A8: dom i = a by CAT_1:5
.= cod g by A7, CAT_1:5 ;
A9: cod gg = cod g by Def12
.= aa by A1, A7, CAT_1:5 ;
then A10: dom (id$ aa) = cod gg ;
[i,g] in dom the Comp of (CohCat X) by A8, CAT_1:def 6;
hence i (*) g = the Comp of (CohCat X) . (i,g) by CAT_1:def 1
.= (id$ aa) * gg by A2, A10, Def13
.= g by A9, Th25 ;
:: thesis:

end;