let h1, h2 be Contravariant_Functor of A, Functors (A,(EnsHom A)); ( ( 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,?>]
; h1 = h2
hence
h1 = h2
by FUNCT_2:63; verum