let C, D, C', D' be Category; :: thesis: for T being Functor of C,D
for T' being Functor of C',D' holds [:T,T':] = <:(T * (pr1 C,C')),(T' * (pr2 C,C')):>
let T be Functor of C,D; :: thesis: for T' being Functor of C',D' holds [:T,T':] = <:(T * (pr1 C,C')),(T' * (pr2 C,C')):>
let T' be Functor of C',D'; :: thesis: [:T,T':] = <:(T * (pr1 C,C')),(T' * (pr2 C,C')):>
( dom T = the carrier' of C & dom T' = the carrier' of C' ) by FUNCT_2:def 1;
hence [:T,T':] = <:(T * (pr1 C,C')),(T' * (pr2 C,C')):> by FUNCT_3:87; :: thesis: verum