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

A4: ( 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;

( [D,P1,P2] `1_3 = D & [D,P1,P2] `3_3 = P2 ) ;

then D = [|F1,F2|] by A1, A2, A4, Def22;

then reconsider P2 = P2 as Functor of [|F1,F2|],C2 ;

P2 = the pullback of F1,F2 `3_3 by A4;

hence the pullback of F1,F2 `3_3 is Functor of [|F1,F2|],C2 ; :: thesis: verum

consider D being strict category, P1 being Functor of D,C1, P2 being Functor of D,C2 such that

A4: ( 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;

( [D,P1,P2] `1_3 = D & [D,P1,P2] `3_3 = P2 ) ;

then D = [|F1,F2|] by A1, A2, A4, Def22;

then reconsider P2 = P2 as Functor of [|F1,F2|],C2 ;

P2 = the pullback of F1,F2 `3_3 by A4;

hence the pullback of F1,F2 `3_3 is Functor of [|F1,F2|],C2 ; :: thesis: verum