let A, B be Category; :: thesis: ( A is discrete implies Functors B,A is discrete )
assume A1: A is discrete ; :: thesis: Functors B,A is discrete
let f be Morphism of (Functors B,A); :: according to NATTRA_1:def 19 :: thesis: ex a being Object of (Functors B,A) st f = id a
f in the carrier' of (Functors B,A) ;
then f in NatTrans B,A by Def18;
then consider F1, F2 being Functor of B,A, t being natural_transformation of F1,F2 such that
A2: f = [[F1,F2],t] and
A3: F1 is_naturally_transformable_to F2 by Def16;
F1 in Funct B,A by CAT_2:def 2;
then reconsider a = F1 as Object of (Functors B,A) by Def18;
take a ; :: thesis: f = id a
F1 is_transformable_to F2 by A3, Def7;
then A4: F1 = F2 by A1, Th49;
then t = id F1 by A1, Th50;
hence f = id a by A2, A4, Def18; :: thesis: verum