A1: rng (Obj F) c= the carrier of D by RELAT_1:def 19;
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 (Obj F) . x in rng (Obj F) by FUNCT_1:def 5;
hence (Obj F) . x is Category by A1, CAT_5:12; :: thesis: verum