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

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