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 st g in Hom (cod f),a holds
h1 . g = g * f ) & ( for g being Morphism of st g in Hom (cod f),a holds
h2 . g = g * f ) implies h1 = h2 )
assume that
A12: for g being Morphism of st g in Hom (cod f),a holds
h1 . g = g * f and
A13: for g being Morphism of st g in Hom (cod f),a holds
h2 . g = g * f ; :: thesis: h1 = h2

now

let x be set ; :: 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 ;
thus h1 . x = g * f by A12, A14
.= h2 . x by A13, A14 ; :: thesis: verum

end;

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