let A be 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)))
let f be Element of the carrier' of A; [[<|(cod f),?>,<|(dom f),?>],<|f,?>] is Element of the carrier' of (Functors (A,(EnsHom A)))
<|(cod f),?> is_naturally_transformable_to <|(dom f),?>
by Th2;
then
[[<|(cod f),?>,<|(dom f),?>],<|f,?>] in NatTrans (A,(EnsHom A))
by NATTRA_1:def 16;
hence
[[<|(cod f),?>,<|(dom f),?>],<|f,?>] is Element of the carrier' of (Functors (A,(EnsHom A)))
by NATTRA_1:def 17; verum