let A be Category; for f being Morphism of A holds f * (id (dom f)) = f
let f be Morphism of A; f * (id (dom f)) = f
reconsider f9 = f as Morphism of dom f, cod f by CAT_1:4;
A1:
Hom ((dom f),(cod f)) <> {}
by CAT_1:2;
Hom ((dom f),(dom f)) <> {}
by CAT_1:27;
hence f * (id (dom f)) =
f9 * (id (dom f))
by A1, CAT_1:def 10
.=
f
by A1, CAT_1:29
;
verum