let C be Category; :: thesis: for b, c being Object of C
for g being Morphism of b,c st Hom b,c <> {} holds
g * (id b) = g
let b, c be Object of C; :: thesis: for g being Morphism of b,c st Hom b,c <> {} holds
g * (id b) = g
let g be Morphism of b,c; :: thesis: ( Hom b,c <> {} implies g * (id b) = g )
assume A1: Hom b,c <> {} ; :: thesis: g * (id b) = g
then g in Hom b,c by Def7;
then dom g = b by Th18;
then A2: g * (id b) = g by Th47;
Hom b,b <> {} by Th55;
hence g * (id b) = g by A1, A2, Def13; :: thesis: verum