let A be Category; :: thesis: 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; :: thesis: [[<|(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; :: thesis: verum