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 2;
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:12, PARTFUN1:def 2;
( dom m = c1 & cod m = c2 ) by A1, CAT_1:5;
hence (I `2) . m is Functor of (I `1) . c2,(I `1) . c1 by A2, FUNCT_1:12; :: thesis: verum