let C be Category; for a, b being Object of C
for f being Morphism of a,b st Hom (a,b) <> {} holds
(id b) * f = f
let a, b be Object of C; for f being Morphism of a,b st Hom (a,b) <> {} holds
(id b) * f = f
let f be Morphism of a,b; ( Hom (a,b) <> {} implies (id b) * f = f )
assume A1:
Hom (a,b) <> {}
; (id b) * f = f
A2:
(id b) (*) f = f
by A1, Def10;
Hom (b,b) <> {}
;
hence
(id b) * f = f
by A1, A2, Def11; verum