theorem Th3: :: YONEDA_1:3

for A being Category
for f being Element of the carrier' of A holds [[<|(cod f),?>,<|(dom f),?>],<|f,?>] is Element of the carrier' of (Functors (A,(EnsHom A)))