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 18 :: 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