let h1, h2 be Contravariant_Functor of A, Functors (A,(EnsHom A)); :: thesis: ( ( for f being Morphism of A holds h1 . f = [[<|(cod f),?>,<|(dom f),?>],<|f,?>] ) & ( for f being Morphism of A holds h2 . f = [[<|(cod f),?>,<|(dom f),?>],<|f,?>] ) implies h1 = h2 )

assume that

A45: for f being Morphism of A holds h1 . f = [[<|(cod f),?>,<|(dom f),?>],<|f,?>] and

A46: for f being Morphism of A holds h2 . f = [[<|(cod f),?>,<|(dom f),?>],<|f,?>] ; :: thesis: h1 = h2

assume that

A45: for f being Morphism of A holds h1 . f = [[<|(cod f),?>,<|(dom f),?>],<|f,?>] and

A46: for f being Morphism of A holds h2 . f = [[<|(cod f),?>,<|(dom f),?>],<|f,?>] ; :: thesis: h1 = h2

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

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

thus h1 . f = [[<|(cod f),?>,<|(dom f),?>],<|f,?>] by A45

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

end;thus h1 . f = [[<|(cod f),?>,<|(dom f),?>],<|f,?>] by A45

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