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

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