let A, B, C be Category; :: thesis: for F, G being Functor of A,[:B,C:] st Pr1 F = Pr1 G & Pr2 F = Pr2 G holds
F = G
let F, G be Functor of A,[:B,C:]; :: thesis: ( Pr1 F = Pr1 G & Pr2 F = Pr2 G implies F = G )
reconsider f = F, g = G as Function of the carrier' of A,[: the carrier' of B, the carrier' of C:] by CAT_2:23;
assume Pr1 F = Pr1 G ; :: thesis: ( not Pr2 F = Pr2 G or F = G )
then A1: (pr1 ( the carrier' of B, the carrier' of C)) * f = Pr1 G by CAT_2:def 10
.= (pr1 ( the carrier' of B, the carrier' of C)) * g by CAT_2:def 10 ;
assume Pr2 F = Pr2 G ; :: thesis: F = G
then (pr2 ( the carrier' of B, the carrier' of C)) * f = Pr2 G by CAT_2:def 11
.= (pr2 ( the carrier' of B, the carrier' of C)) * g by CAT_2:def 11 ;
hence F = G by A1, Th5; :: thesis: verum