let V be non empty set ; :: thesis: 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; :: thesis: 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; :: thesis: 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; :: thesis: ( 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 ; :: thesis: (hom-? V,a) . f = [[(Hom (cod f),a),(Hom (dom f),a)],(hom f,a)]
hence (hom-? V,a) . f = (hom-? a) . f by Def27
.= [[(Hom (cod f),a),(Hom (dom f),a)],(hom f,a)] by Def23 ;
:: thesis: verum