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 :: thesis: for x being object st x in Hom ((cod f),(dom g)) holds
h1 . x = h2 . x
let x be object ; :: 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:12; :: thesis: verum