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 (a,c) 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 (a,c) 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 (a,c) holds

(hom?- a) . (id c) = id d )

A1: Hom (a,c) in Hom C ;

assume Hom C c= V ; :: thesis: 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); :: thesis: ( d = Hom (a,c) implies (hom?- a) . (id c) = id d )

assume d = Hom (a,c) ; :: thesis: (hom?- a) . (id c) = id d

hence (hom?- a) . (id c) = id$ (@ d) by A2, Def20

.= id d by Th28 ;

:: thesis: verum

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; :: thesis: 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; :: thesis: ( 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 ; :: thesis: 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); :: thesis: ( d = Hom (a,c) implies (hom?- a) . (id c) = id d )

assume d = Hom (a,c) ; :: thesis: (hom?- a) . (id c) = id d

hence (hom?- a) . (id c) = id$ (@ d) by A2, Def20

.= id d by Th28 ;

:: thesis: verum