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 f' = f as Morphism of dom f, cod f by CAT_1:22;
A1: ( Hom (dom f),(cod f) <> {} & Hom (dom f),(dom f) <> {} ) by CAT_1:19, CAT_1:56;
hence f * (id (dom f)) = f' * (id (dom f)) by CAT_1:def 13
.= f by A1, CAT_1:58 ;
:: thesis: verum