let V be non empty set ; :: thesis: for C being Category
for a, b being Object of C st Hom C c= V holds
(Obj (hom-? V,a)) . b = Hom b,a
let C be Category; :: thesis: for a, b being Object of C st Hom C c= V holds
(Obj (hom-? V,a)) . b = Hom b,a
let a, b be Object of C; :: thesis: ( Hom C c= V implies (Obj (hom-? V,a)) . b = Hom b,a )
assume A1: Hom C c= V ; :: thesis: (Obj (hom-? V,a)) . b = Hom b,a
Hom b,a in Hom C ;
then reconsider A = Hom b,a as Element of V by A1;
set d = @ A;
(hom-? V,a) . (id b) = (hom-? a) . (id b) by A1, Def27
.= id (@ A) by A1, Lm9 ;
hence (Obj (hom-? V,a)) . b = Hom b,a by OPPCAT_1:31; :: thesis: verum