let V be non empty set ; :: thesis: for C being Category

for f, g being Morphism of C st Hom C c= V holds

(hom?? (V,C)) . [(f opp),g] = [[(Hom ((cod f),(dom g))),(Hom ((dom f),(cod g)))],(hom (f,g))]

let C be Category; :: thesis: for f, g being Morphism of C st Hom C c= V holds

(hom?? (V,C)) . [(f opp),g] = [[(Hom ((cod f),(dom g))),(Hom ((dom f),(cod g)))],(hom (f,g))]

let f, g be Morphism of C; :: thesis: ( Hom C c= V implies (hom?? (V,C)) . [(f opp),g] = [[(Hom ((cod f),(dom g))),(Hom ((dom f),(cod g)))],(hom (f,g))] )

assume A1: Hom C c= V ; :: thesis: (hom?? (V,C)) . [(f opp),g] = [[(Hom ((cod f),(dom g))),(Hom ((dom f),(cod g)))],(hom (f,g))]

thus (hom?? (V,C)) . [(f opp),g] = (hom?? C) . [f,g] by A1, Def26

.= [[(Hom ((cod f),(dom g))),(Hom ((dom f),(cod g)))],(hom (f,g))] by Def23 ; :: thesis: verum

for f, g being Morphism of C st Hom C c= V holds

(hom?? (V,C)) . [(f opp),g] = [[(Hom ((cod f),(dom g))),(Hom ((dom f),(cod g)))],(hom (f,g))]

let C be Category; :: thesis: for f, g being Morphism of C st Hom C c= V holds

(hom?? (V,C)) . [(f opp),g] = [[(Hom ((cod f),(dom g))),(Hom ((dom f),(cod g)))],(hom (f,g))]

let f, g be Morphism of C; :: thesis: ( Hom C c= V implies (hom?? (V,C)) . [(f opp),g] = [[(Hom ((cod f),(dom g))),(Hom ((dom f),(cod g)))],(hom (f,g))] )

assume A1: Hom C c= V ; :: thesis: (hom?? (V,C)) . [(f opp),g] = [[(Hom ((cod f),(dom g))),(Hom ((dom f),(cod g)))],(hom (f,g))]

thus (hom?? (V,C)) . [(f opp),g] = (hom?? C) . [f,g] by A1, Def26

.= [[(Hom ((cod f),(dom g))),(Hom ((dom f),(cod g)))],(hom (f,g))] by Def23 ; :: thesis: verum