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