let C be Category; for a being Object of C
for f being Morphism of C holds
( hom (id a),f = hom a,f & hom f,(id a) = hom f,a )
let a be Object of C; for f being Morphism of C holds
( hom (id a),f = hom a,f & hom f,(id a) = hom f,a )
let f be Morphism of C; ( hom (id a),f = hom a,f & hom f,(id a) = hom f,a )
A1:
cod (id a) = a
by CAT_1:44;
A2:
dom (id a) = a
by CAT_1:44;
now
Hom (dom f),
(cod f) <> {}
by CAT_1:19;
then
(
Hom a,
(cod f) = {} implies
Hom a,
(dom f) = {} )
by CAT_1:52;
hence
(
dom (hom (id a),f) = Hom a,
(dom f) &
dom (hom a,f) = Hom a,
(dom f) )
by A2, A1, FUNCT_2:def 1;
for x being set st x in Hom a,(dom f) holds
(hom (id a),f) . x = (hom a,f) . xlet x be
set ;
( x in Hom a,(dom f) implies (hom (id a),f) . x = (hom a,f) . x )assume A3:
x in Hom a,
(dom f)
;
(hom (id a),f) . x = (hom a,f) . xthen reconsider g =
x as
Morphism of
C ;
A4:
dom g = a
by A3, CAT_1:18;
A5:
cod g = dom f
by A3, CAT_1:18;
thus (hom (id a),f) . x =
(f * g) * (id a)
by A1, A3, Def24
.=
f * (g * (id a))
by A1, A4, A5, CAT_1:43
.=
f * g
by A4, CAT_1:47
.=
(hom a,f) . x
by A3, Def20
;
verum end;
hence
hom (id a),f = hom a,f
by FUNCT_1:9; hom f,(id a) = hom f,a
now
Hom (dom f),
(cod f) <> {}
by CAT_1:19;
then
(
Hom (dom f),
a = {} implies
Hom (cod f),
a = {} )
by CAT_1:52;
hence
(
dom (hom f,(id a)) = Hom (cod f),
a &
dom (hom f,a) = Hom (cod f),
a )
by A2, A1, FUNCT_2:def 1;
for x being set st x in Hom (cod f),a holds
(hom f,(id a)) . x = (hom f,a) . xlet x be
set ;
( x in Hom (cod f),a implies (hom f,(id a)) . x = (hom f,a) . x )assume A6:
x in Hom (cod f),
a
;
(hom f,(id a)) . x = (hom f,a) . xthen reconsider g =
x as
Morphism of
C ;
A7:
cod g = a
by A6, CAT_1:18;
thus (hom f,(id a)) . x =
((id a) * g) * f
by A2, A6, Def24
.=
g * f
by A7, CAT_1:46
.=
(hom f,a) . x
by A6, Def21
;
verum end;
hence
hom f,(id a) = hom f,a
by FUNCT_1:9; verum