dom ((I `1 ) * the Source of C) = the carrier' of C by PARTFUN1:def 4;
then ( 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;
hence (I `2 ) . m is Functor of (I `1 ) . (dom m),(I `1 ) . (cod m) by FUNCT_1:22; :: thesis: verum