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 (a,(dom f))),(Hom (a,(cod f)))],(hom (a,f))]
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 (a,(dom f))),(Hom (a,(cod f)))],(hom (a,f))]
let a be Object of C; :: thesis: for f being Morphism of C st Hom C c= V holds
(hom?- (V,a)) . f = [[(Hom (a,(dom f))),(Hom (a,(cod f)))],(hom (a,f))]
let f be Morphism of C; :: thesis: ( Hom C c= V implies (hom?- (V,a)) . f = [[(Hom (a,(dom f))),(Hom (a,(cod f)))],(hom (a,f))] )
assume Hom C c= V ; :: thesis: (hom?- (V,a)) . f = [[(Hom (a,(dom f))),(Hom (a,(cod f)))],(hom (a,f))]
hence (hom?- (V,a)) . f = (hom?- a) . f by Def24
.= [[(Hom (a,(dom f))),(Hom (a,(cod f)))],(hom (a,f))] by Def20 ;
:: thesis: verum