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 Th3;
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 18; :: thesis: verum