let C be Category; :: thesis: for I being Indexing of C
for D being Categorial Category holds
( rng I is Subcategory of D iff D is TargetCat of I )
let I be Indexing of C; :: thesis: for D being Categorial Category holds
( rng I is Subcategory of D iff D is TargetCat of I )
let D be Categorial Category; :: thesis: ( rng I is Subcategory of D iff D is TargetCat of I )

hereby :: thesis: ( D is TargetCat of I implies rng I is Subcategory of D )

assume A1: rng I is Subcategory of D ; :: thesis: D is TargetCat of I
thus D is TargetCat of I :: thesis: verum

proof

hereby :: according to INDEX_1:def 9 :: thesis: for b being Element of the carrier' of C holds [[((I `1) . ( the Source of C . b)),((I `1) . ( the Target of C . b))],((I `2) . b)] is Morphism of D

let a be Object of C; :: thesis: (I `1) . a is Object of D
(I `1) . a is Object of (rng I) by Def9;
hence (I `1) . a is Object of D by A1, CAT_2:6; :: thesis: verum

end;

let b be Morphism of C; :: thesis: [[((I `1) . ( the Source of C . b)),((I `1) . ( the Target of C . b))],((I `2) . b)] is Morphism of D
[[((I `1) . ( the Source of C . b)),((I `1) . ( the Target of C . b))],((I `2) . b)] is Morphism of (rng I) by Def9;
hence [[((I `1) . ( the Source of C . b)),((I `1) . ( the Target of C . b))],((I `2) . b)] is Morphism of D by A1, CAT_2:8; :: thesis: verum

end;

end;

assume D is TargetCat of I ; :: thesis: rng I is Subcategory of D
then reconsider T = D as TargetCat of I ;
rng I = Image (I -functor (C,T)) by Def12;
hence rng I is Subcategory of D ; :: thesis: verum