( dom ((I `1 ) * the Source of C) = the carrier' of C & dom ((I `1 ) * the Target of C) = the carrier' of C ) by PBOOLE:def 3;
then ( ((I `1 ) * the Source of C) . m = (I `1 ) . (the Source of C . m) & ((I `1 ) * the Target of C) . m = (I `1 ) . (the Target of C . m) ) by FUNCT_1:22;
hence (I `2 ) . m is Functor of (I `1 ) . (cod m),(I `1 ) . (dom m) ; :: thesis: verum