let C be Category; :: thesis: for I being Indexing of C
for c1, c2 being Object of C st not Hom c1,c2 is empty holds
for m being Morphism of c1,c2 holds (I `2 ) . m is Functor of (I `1 ) . c1,(I `1 ) . c2
let I be Indexing of C; :: thesis: for c1, c2 being Object of C st not Hom c1,c2 is empty holds
for m being Morphism of c1,c2 holds (I `2 ) . m is Functor of (I `1 ) . c1,(I `1 ) . c2
let c1, c2 be Object of C; :: thesis: ( not Hom c1,c2 is empty implies for m being Morphism of c1,c2 holds (I `2 ) . m is Functor of (I `1 ) . c1,(I `1 ) . c2 )
assume A1: not Hom c1,c2 is empty ; :: thesis: for m being Morphism of c1,c2 holds (I `2 ) . m is Functor of (I `1 ) . c1,(I `1 ) . c2
let m be Morphism of c1,c2; :: thesis: (I `2 ) . m is Functor of (I `1 ) . c1,(I `1 ) . c2
dom ((I `1 ) * the Source of C) = the carrier' of C by PARTFUN1:def 4;
then A2: ( dom ((I `1 ) * the Target of C) = the carrier' of C & ((I `1 ) * the Source of C) . m = (I `1 ) . (the Source of C . m) ) by FUNCT_1:22, PARTFUN1:def 4;
( dom m = c1 & cod m = c2 ) by A1, CAT_1:23;
hence (I `2 ) . m is Functor of (I `1 ) . c1,(I `1 ) . c2 by A2, FUNCT_1:22; :: thesis: verum