let x be set ; :: according to INDEX_1:def 1 :: thesis: ( x in dom (Obj F) implies (Obj F) . x is Category )
assume x in dom (Obj F) ; :: thesis: (Obj F) . x is Category
then ( rng (Obj F) c= the carrier of D & (Obj F) . x in rng (Obj F) ) by FUNCT_1:def 3, RELAT_1:def 19;
hence (Obj F) . x is Category by CAT_5:12; :: thesis: verum