set T = the pullback of F1,F2;
consider D being strict category, P1 being Functor of D,C1, P2 being Functor of D,C2 such that
A3:
( the pullback of F1,F2 = [D,P1,P2] & P1 is covariant & P2 is covariant & D,P1,P2 is_pullback_of F1,F2 )
by A1, A2, Def21;
thus
the pullback of F1,F2 `1_3 is strict category
by A3; verum