let C be Category; :: thesis: for I being coIndexing 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 ) . c2,(I `1 ) . c1
let I be coIndexing 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 ) . c2,(I `1 ) . c1
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 ) . c2,(I `1 ) . c1 )
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 ) . c2,(I `1 ) . c1
let m be Morphism of c1,c2; :: thesis: (I `2 ) . m is Functor of (I `1 ) . c2,(I `1 ) . c1
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 ) . c2,(I `1 ) . c1 by A2, FUNCT_1:22; :: thesis: verum