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:30; :: 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) = {}
set m = the Element of Hom (a,b);
assume A4: Hom (a,b) <> {} ; :: thesis: contradiction
then reconsider m = the Element of Hom (a,b) 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:26;
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 18 :: 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:42;
take dom f ; :: thesis: f = id (dom f)
A10: id (dom f) in Hom ((dom f),(dom f)) by CAT_1:26;
Hom ((dom f),(cod f)) <> {} by CAT_1:2;
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