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

let x be set ; :: 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:18; :: thesis: verum