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))); :: thesis: ( ( 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 ; :: thesis: h1 = h2

now :: thesis: for x being object st x in Hom (a,(dom f)) holds
h1 . x = h2 . x

let x be object ; :: thesis: ( x in Hom (a,(dom f)) implies h1 . x = h2 . x )
assume A7: x in Hom (a,(dom f)) ; :: thesis: h1 . x = h2 . x
then reconsider g = x as Morphism of C ;
thus h1 . x = f (*) g by A5, A7
.= h2 . x by A6, A7 ; :: thesis: verum

end;

hence h1 = h2 by FUNCT_2:12; :: thesis: verum