let C be Category; for a, c being Object of C holds hom (a,(id c)) = id (Hom (a,c))
let a, c be Object of C; hom (a,(id c)) = id (Hom (a,c))
set A = Hom (a,c);
now ( dom (hom (a,(id c))) = Hom (a,c) & ( for x being object st x in Hom (a,c) holds
(hom (a,(id c))) . x = x ) )
(
Hom (
a,
c)
= {} implies
Hom (
a,
c)
= {} )
;
hence
dom (hom (a,(id c))) = Hom (
a,
c)
by FUNCT_2:def 1;
for x being object st x in Hom (a,c) holds
(hom (a,(id c))) . x = xlet x be
object ;
( x in Hom (a,c) implies (hom (a,(id c))) . x = x )assume A1:
x in Hom (
a,
c)
;
(hom (a,(id c))) . x = xthen reconsider g =
x as
Morphism of
C ;
A2:
cod g = c
by A1, CAT_1:1;
thus (hom (a,(id c))) . x =
(id c) (*) g
by A1, Def18
.=
x
by A2, CAT_1:21
;
verum end;
hence
hom (a,(id c)) = id (Hom (a,c))
by FUNCT_1:17; verum