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 19 :: thesis: ex a being Object of C st f = id a
reconsider f' = f as Morphism of A by CAT_2:14;
consider a' being Object of A such that
A1: f' = id a' by Def19;
take dom f ; :: thesis: f = id (dom f)
dom f' = a' by A1, CAT_1:44;
then dom f = a' by CAT_2:15;
hence f = id (dom f) by A1, CAT_2:def 4; :: thesis: verum