let o, m be set ; :: thesis: 1Cat o,m is discrete
let f be Morphism of ; :: according to NATTRA_1:def 19 :: thesis: ex a being Object of st f = id a
consider a being Object of ;
f = m by TARSKI:def 1
.= id a by TARSKI:def 1 ;
hence ex a being Object of st f = id a ; :: thesis: verum