let A be Category; :: thesis: for f being Morphism of A holds f (*) (id (dom f)) = f
let f be Morphism of A; :: thesis: 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)) <> {} ;
hence f (*) (id (dom f)) = f9 * (id (dom f)) by A1, CAT_1:def 13
.= f by A1, CAT_1:29 ;
:: thesis: verum