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

now

let x be set ; :: thesis: ( x in Hom (cod f),(dom g) implies h1 . x = h2 . x )
assume A9: x in Hom (cod f),(dom g) ; :: thesis: h1 . x = h2 . x
then reconsider h = x as Morphism of C ;
thus h1 . x = (g * h) * f by A7, A9
.= h2 . x by A8, A9 ; :: thesis: verum

end;

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