let V be non empty set ; :: thesis: 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 (c,a) holds
(hom-? a) . (id c) = id d
let C be Category; :: thesis: for a, c 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 a, c 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 )
A1: Hom (c,a) in Hom C ;
assume Hom C c= V ; :: thesis: for d being Object of (Ens V) st d = Hom (c,a) holds
(hom-? a) . (id c) = id d
then reconsider A = Hom (c,a) as Element of V by A1;
A2: hom ((id c),a) = id A by Th43;
let d be Object of (Ens V); :: thesis: ( d = Hom (c,a) implies (hom-? a) . (id c) = id d )
assume d = Hom (c,a) ; :: thesis: (hom-? a) . (id c) = id d
hence (hom-? a) . (id c) = id$ (@ d) by A2, Def21
.= id d by Th28 ;
:: thesis: verum