set X = Hom (a,(dom f));

set Y = Hom (a,(cod f));

let h1, h2 be Function of (Hom (a,(dom f))),(Hom (a,(cod f))); :: thesis: ( ( for g being Morphism of C st g in Hom (a,(dom f)) holds

h1 . g = f (*) g ) & ( for g being Morphism of C st g in Hom (a,(dom f)) holds

h2 . g = f (*) g ) implies h1 = h2 )

assume that

A5: for g being Morphism of C st g in Hom (a,(dom f)) holds

h1 . g = f (*) g and

A6: for g being Morphism of C st g in Hom (a,(dom f)) holds

h2 . g = f (*) g ; :: thesis: h1 = h2

set Y = Hom (a,(cod f));

let h1, h2 be Function of (Hom (a,(dom f))),(Hom (a,(cod f))); :: thesis: ( ( for g being Morphism of C st g in Hom (a,(dom f)) holds

h1 . g = f (*) g ) & ( for g being Morphism of C st g in Hom (a,(dom f)) holds

h2 . g = f (*) g ) implies h1 = h2 )

assume that

A5: for g being Morphism of C st g in Hom (a,(dom f)) holds

h1 . g = f (*) g and

A6: for g being Morphism of C st g in Hom (a,(dom f)) holds

h2 . g = f (*) g ; :: thesis: h1 = h2

now :: thesis: for x being object st x in Hom (a,(dom f)) 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 (a,(dom f)) implies h1 . x = h2 . x )

assume A7: x in Hom (a,(dom f)) ; :: thesis: h1 . x = h2 . x

then reconsider g = x as Morphism of C ;

thus h1 . x = f (*) g by A5, A7

.= h2 . x by A6, A7 ; :: thesis: verum

end;assume A7: x in Hom (a,(dom f)) ; :: thesis: h1 . x = h2 . x

then reconsider g = x as Morphism of C ;

thus h1 . x = f (*) g by A5, A7

.= h2 . x by A6, A7 ; :: thesis: verum