set X = Hom ((cod f),a);
set Y = Hom ((dom f),a);
let h1, h2 be Function of (Hom ((cod f),a)),(Hom ((dom f),a)); :: thesis: ( ( for g being Morphism of C st g in Hom ((cod f),a) holds
h1 . g = g (*) f ) & ( for g being Morphism of C st g in Hom ((cod f),a) holds
h2 . g = g (*) f ) implies h1 = h2 )
assume that
A12: for g being Morphism of C st g in Hom ((cod f),a) holds
h1 . g = g (*) f and
A13: for g being Morphism of C st g in Hom ((cod f),a) holds
h2 . g = g (*) f ; :: thesis: h1 = h2

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

let x be object ; :: thesis: ( x in Hom ((cod f),a) implies h1 . x = h2 . x )
assume A14: x in Hom ((cod f),a) ; :: thesis: h1 . x = h2 . x
then reconsider g = x as Morphism of C ;
thus h1 . x = g (*) f by A12, A14
.= h2 . x by A13, A14 ; :: thesis: verum

end;

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