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