let A be discrete Category; :: thesis: for C being Subcategory of A holds C is discrete
let C be Subcategory of A; :: thesis: C is discrete
let f be Morphism of C; :: according to NATTRA_1:def 18 :: thesis: ex a being Object of C st f = id a
reconsider f9 = f as Morphism of A by CAT_2:8;
take dom f ; :: thesis: f = id (dom f)
consider a9 being Object of A such that
A1: f9 = id a9 by Def19;
dom f9 = a9 by A1, CAT_1:19;
then dom f = a9 by CAT_2:9;
hence f = id (dom f) by A1, CAT_2:def 4; :: thesis: verum