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

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

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

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

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

assume that

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

h1 . g = g (*) f and

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

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

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

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

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

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

assume that

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

h1 . g = g (*) f and

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

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

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

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

then reconsider g = x as Morphism of C ;

thus h1 . x = g (*) f by A12, A14

.= h2 . x by A13, A14 ; :: thesis: verum

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

then reconsider g = x as Morphism of C ;

thus h1 . x = g (*) f by A12, A14

.= h2 . x by A13, A14 ; :: thesis: verum