let h1, h2 be Function of the carrier' of C,(Maps (Hom C)); :: thesis: ( ( for f being Morphism of C holds h1 . f = [[(Hom (a,(dom f))),(Hom (a,(cod f)))],(hom (a,f))] ) & ( for f being Morphism of C holds h2 . f = [[(Hom (a,(dom f))),(Hom (a,(cod f)))],(hom (a,f))] ) implies h1 = h2 )

assume that

A4: for f being Morphism of C holds h1 . f = [[(Hom (a,(dom f))),(Hom (a,(cod f)))],(hom (a,f))] and

A5: for f being Morphism of C holds h2 . f = [[(Hom (a,(dom f))),(Hom (a,(cod f)))],(hom (a,f))] ; :: thesis: h1 = h2

assume that

A4: for f being Morphism of C holds h1 . f = [[(Hom (a,(dom f))),(Hom (a,(cod f)))],(hom (a,f))] and

A5: for f being Morphism of C holds h2 . f = [[(Hom (a,(dom f))),(Hom (a,(cod f)))],(hom (a,f))] ; :: thesis: h1 = h2

now :: thesis: for f being Morphism of C holds h1 . f = h2 . f

hence
h1 = h2
by FUNCT_2:63; :: thesis: verumlet f be Morphism of C; :: thesis: h1 . f = h2 . f

thus h1 . f = [[(Hom (a,(dom f))),(Hom (a,(cod f)))],(hom (a,f))] by A4

.= h2 . f by A5 ; :: thesis: verum

end;thus h1 . f = [[(Hom (a,(dom f))),(Hom (a,(cod f)))],(hom (a,f))] by A4

.= h2 . f by A5 ; :: thesis: verum