set X = Hom (a,(dom f));
set Y = Hom (a,(cod f));
let h1, h2 be Function of (Hom (a,(dom f))),(Hom (a,(cod f))); ( ( for g being Morphism of C st g in Hom (a,(dom f)) holds
h1 . g = f (*) g ) & ( for g being Morphism of C st g in Hom (a,(dom f)) holds
h2 . g = f (*) g ) implies h1 = h2 )
assume that
A5:
for g being Morphism of C st g in Hom (a,(dom f)) holds
h1 . g = f (*) g
and
A6:
for g being Morphism of C st g in Hom (a,(dom f)) holds
h2 . g = f (*) g
; h1 = h2
hence
h1 = h2
by FUNCT_2:12; verum