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