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

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

hence
h1 = h2
by FUNCT_2:12; :: thesis: verumh1 . 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;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