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:] ;
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
.= (pr1 ( the carrier' of B, the carrier' of C)) * g ;
assume Pr2 F = Pr2 G ; :: thesis: F = G
then (pr2 ( the carrier' of B, the carrier' of C)) * f = Pr2 G
.= (pr2 ( the carrier' of B, the carrier' of C)) * g ;
hence F = G by A1, FUNCT_3:80; :: thesis: verum