A1: dom f = f `11 by CAT_5:2;
( f `11 = cat (f `11) & f `12 = cat (f `12) ) by CAT_5:def 7;
hence f `2 is Functor of f `11 ,f `12 by A1, CAT_5:2; :: thesis: verum