let V be non empty set ; :: thesis: for C being Category
for c, a being Object of C st Hom C c= V holds
for d being Object of (Ens V) st d = Hom c,a holds
(hom-? a) . (id c) = id d
let C be Category; :: thesis: for c, a being Object of C st Hom C c= V holds
for d being Object of (Ens V) st d = Hom c,a holds
(hom-? a) . (id c) = id d
let c, a be Object of C; :: thesis: ( Hom C c= V implies for d being Object of (Ens V) st d = Hom c,a holds
(hom-? a) . (id c) = id d )
assume A1: Hom C c= V ; :: thesis: for d being Object of (Ens V) st d = Hom c,a holds
(hom-? a) . (id c) = id d
let d be Object of (Ens V); :: thesis: ( d = Hom c,a implies (hom-? a) . (id c) = id d )
assume A2: d = Hom c,a ; :: thesis: (hom-? a) . (id c) = id d
Hom c,a in Hom C ;
then reconsider A = Hom c,a as Element of V by A1;
( dom (id c) = c & cod (id c) = c & hom (id c),a = id A ) by Th44, CAT_1:44;
hence (hom-? a) . (id c) = id$ (@ d) by A2, Def23
.= id d by Def13 ;
:: thesis: verum