let V be non empty set ; for C being Category
for a being Object of C
for f being Morphism of C st Hom C c= V holds
(hom-? (V,a)) . f = [[(Hom ((cod f),a)),(Hom ((dom f),a))],(hom (f,a))]
let C be Category; for a being Object of C
for f being Morphism of C st Hom C c= V holds
(hom-? (V,a)) . f = [[(Hom ((cod f),a)),(Hom ((dom f),a))],(hom (f,a))]
let a be Object of C; for f being Morphism of C st Hom C c= V holds
(hom-? (V,a)) . f = [[(Hom ((cod f),a)),(Hom ((dom f),a))],(hom (f,a))]
let f be Morphism of C; ( Hom C c= V implies (hom-? (V,a)) . f = [[(Hom ((cod f),a)),(Hom ((dom f),a))],(hom (f,a))] )
assume
Hom C c= V
; (hom-? (V,a)) . f = [[(Hom ((cod f),a)),(Hom ((dom f),a))],(hom (f,a))]
hence (hom-? (V,a)) . f =
(hom-? a) . f
by Def25
.=
[[(Hom ((cod f),a)),(Hom ((dom f),a))],(hom (f,a))]
by Def21
;
verum