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))); ( ( 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
; h1 = h2
hence
h1 = h2
by FUNCT_2:12; verum