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 = {}
consider m being Element of Hom a,b;
assume A4: Hom a,b <> {} ; :: thesis: contradiction
then reconsider m = m as Morphism of A by 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 A6: Hom c,c meets Hom a,b by A4, A5, XBOOLE_0:3;
then c = a by Th17;
hence contradiction by A3, A6, Th17; :: thesis: verum

end;

assume that
A7: for a being Object of A ex B being finite set st
( B = Hom a,a & card B = 1 ) and
A8: 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
ex B being finite set st
( B = Hom (dom f),(dom f) & card B = 1 ) by A7;
then consider x being set such that
A9: Hom (dom f),(dom f) = {x} by CARD_2:60;
take dom f ; :: thesis: f = id (dom f)
A10: id (dom f) in Hom (dom f),(dom f) by CAT_1:55;
Hom (dom f),(cod f) <> {} by CAT_1:19;
then dom f = cod f by A8;
then f in Hom (dom f),(dom f) ;
then f = x by A9, TARSKI:def 1;
hence f = id (dom f) by A9, A10, TARSKI:def 1; :: thesis: verum