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 Def25
.= [[(Hom ((cod f),a)),(Hom ((dom f),a))],(hom (f,a))] by Def21 ;
:: thesis: verum