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