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 dom (id b) = cod f by Def8;
then the Comp of C . ((id b),f) = (id b) * f by Th41;
hence (id b) * f = f by A1, Def8; :: thesis: verum