let V be non empty set ; for C being Category
for a, c being Object of C st Hom C c= V holds
for d being Object of (Ens V) st d = Hom (a,c) holds
(hom?- a) . (id c) = id d
let C be Category; for a, c being Object of C st Hom C c= V holds
for d being Object of (Ens V) st d = Hom (a,c) holds
(hom?- a) . (id c) = id d
let a, c be Object of C; ( Hom C c= V implies for d being Object of (Ens V) st d = Hom (a,c) holds
(hom?- a) . (id c) = id d )
A1:
Hom (a,c) in Hom C
;
assume
Hom C c= V
; for d being Object of (Ens V) st d = Hom (a,c) holds
(hom?- a) . (id c) = id d
then reconsider A = Hom (a,c) as Element of V by A1;
A2:
hom (a,(id c)) = id A
by Th42;
let d be Object of (Ens V); ( d = Hom (a,c) implies (hom?- a) . (id c) = id d )
assume
d = Hom (a,c)
; (hom?- a) . (id c) = id d
hence (hom?- a) . (id c) =
id$ (@ d)
by A2, Def20
.=
id d
by Th28
;
verum