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
A48: for f being Morphism of A holds h1 . f = [[<|(cod f),?>,<|(dom f),?>],<|f,?>] and
A49: for f being Morphism of A holds h2 . f = [[<|(cod f),?>,<|(dom f),?>],<|f,?>] ; :: thesis: h1 = h2

now

let f be Morphism of A; :: thesis: h1 . f = h2 . f
thus h1 . f = [[<|(cod f),?>,<|(dom f),?>],<|f,?>] by A48
.= h2 . f by A49 ; :: thesis: verum

end;

hence h1 = h2 by FUNCT_2:113; :: thesis: verum