let C be Category; 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; 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; ( 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
; 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; (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 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) . c1,(I `1) . c2
by A2, FUNCT_1:12; verum