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