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 )
the carrier' of [:B,C:] = [:the carrier' of B,the carrier' of C:] by CAT_2:33;
then 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 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