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