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