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