let A be Category; :: thesis: for f being Morphism of holds (id (cod f)) * f = f
let f be Morphism of ; :: thesis: (id (cod f)) * f = f
reconsider f' = f as Morphism of dom f, cod f by CAT_1:22;
A1: Hom (dom f),(cod f) <> {} by CAT_1:19;
Hom (cod f),(cod f) <> {} by CAT_1:56;
hence (id (cod f)) * f = (id (cod f)) * f' by A1, CAT_1:def 13
.= f by A1, CAT_1:57 ;
:: thesis: verum