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