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