let A be Category; :: thesis: ( A is discrete iff ( ( for a being Object of A ex B being finite set st
( B = Hom a,a & card B = 1 ) ) & ( for a, b being Object of A st a <> b holds
Hom a,b = {} ) ) )
thus ( A is discrete implies ( ( for a being Object of A ex B being finite set st
( B = Hom a,a & card B = 1 ) ) & ( for a, b being Object of A st a <> b holds
Hom a,b = {} ) ) ) :: thesis: ( ( for a being Object of A ex B being finite set st
( B = Hom a,a & card B = 1 ) ) & ( for a, b being Object of A st a <> b holds
Hom a,b = {} ) implies A is discrete )

proof

assume A1: A is discrete ; :: thesis: ( ( for a being Object of A ex B being finite set st
( B = Hom a,a & card B = 1 ) ) & ( for a, b being Object of A st a <> b holds
Hom a,b = {} ) )

hereby :: thesis: for a, b being Object of A st a <> b holds
Hom a,b = {}

let a be Object of A; :: thesis: ex B being finite set st
( B = Hom a,a & card B = 1 )
A2: Hom a,a = {(id a)} by A1, Th44;
then reconsider B = Hom a,a as finite set ;
take B = B; :: thesis: ( B = Hom a,a & card B = 1 )
thus B = Hom a,a ; :: thesis: card B = 1
thus card B = 1 by A2, CARD_1:50; :: thesis: verum

end;

let a, b be Object of A; :: thesis: ( a <> b implies Hom a,b = {} )
assume A3: a <> b ; :: thesis: Hom a,b = {}
assume A4: Hom a,b <> {} ; :: thesis: contradiction
consider m being Element of Hom a,b;
reconsider m = m as Morphism of A by A4, TARSKI:def 3;
consider c being Object of A such that
A5: m = id c by A1, Def19;
id c in Hom c,c by CAT_1:55;
then Hom c,c meets Hom a,b by A4, A5, XBOOLE_0:3;
then ( c = a & c = b ) by Th17;
hence contradiction by A3; :: thesis: verum

end;

assume A6: ( ( for a being Object of A ex B being finite set st
( B = Hom a,a & card B = 1 ) ) & ( for a, b being Object of A st a <> b holds
Hom a,b = {} ) ) ; :: thesis: A is discrete
let f be Morphism of A; :: according to NATTRA_1:def 19 :: thesis: ex a being Object of A st f = id a
take dom f ; :: thesis: f = id (dom f)
consider B being finite set such that
A7: ( B = Hom (dom f),(dom f) & card B = 1 ) by A6;
Hom (dom f),(cod f) <> {} by CAT_1:19;
then A8: dom f = cod f by A6;
consider x being set such that
A9: Hom (dom f),(dom f) = {x} by A7, CARD_2:60;
( f in Hom (dom f),(dom f) & id (dom f) in Hom (dom f),(dom f) ) by A8, CAT_1:55;
then ( f = x & id (dom f) = x ) by A9, TARSKI:def 1;
hence f = id (dom f) ; :: thesis: verum