the carrier of C is categorial by Def6;
then reconsider A = dom m, B = cod m as Category ;
consider F being Functor of A,B such that
A1: m = [[A,B],F] by Def6;
A2: m `2 = F by A1;
cat A = A by Def7;
hence m `2 is Functor of cat (dom m), cat (cod m) by A2, Def7; :: thesis: verum