let C be Category; :: thesis: for b being Object of C
for f being Morphism of C st cod f = b holds
(id b) (*) f = f
let b be Object of C; :: thesis: for f being Morphism of C st cod f = b holds
(id b) (*) f = f
let f be Morphism of C; :: thesis: ( cod f = b implies (id b) (*) f = f )
assume A1: cod f = b ; :: thesis: (id b) (*) f = f
then reconsider ff = f as Morphism of dom f,b by Th3;
Hom ((dom f),b) <> {} by A1, Th1;
then (id b) (*) ff = ff by Def10;
hence (id b) (*) f = f ; :: thesis: verum