let
C
be
Category
;
:: thesis:
for
a
,
b
being
Object
of
C
holds
hom
(
(
id
a
)
,
(
id
b
)
)
=
id
(
Hom
(
a
,
b
)
)
let
a
,
b
be
Object
of
C
;
:: thesis:
hom
(
(
id
a
)
,
(
id
b
)
)
=
id
(
Hom
(
a
,
b
)
)
thus
hom
(
(
id
a
)
,
(
id
b
)
) =
hom
(
a
,
(
id
b
)
)
by
Th52
.=
id
(
Hom
(
a
,
b
)
)
by
Th42
;
:: thesis:
verum