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

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