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
A2: g (*) (id b) = g by A1, Def10;
Hom (b,b) <> {} ;
hence g * (id b) = g by A1, A2, Def11; :: thesis: verum