let A, B, C be Category; :: thesis: for F being Functor of A,B
for G being Functor of A,C holds
( Pr1 <:F,G:> = F & Pr2 <:F,G:> = G )
let F be Functor of A,B; :: thesis: for G being Functor of A,C holds
( Pr1 <:F,G:> = F & Pr2 <:F,G:> = G )
let G be Functor of A,C; :: thesis: ( Pr1 <:F,G:> = F & Pr2 <:F,G:> = G )
thus Pr1 <:F,G:> = (pr1 ( the carrier' of B, the carrier' of C)) * <:F,G:> by CAT_2:def 10
.= F by FUNCT_3:62 ; :: thesis: Pr2 <:F,G:> = G
thus Pr2 <:F,G:> = (pr2 ( the carrier' of B, the carrier' of C)) * <:F,G:> by CAT_2:def 11
.= G by FUNCT_3:62 ; :: thesis: verum