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:] is Functor of [:C,C9:],[:D,D9:]
let T be Functor of C,D; :: thesis: for T9 being Functor of C9,D9 holds [:T,T9:] is Functor of [:C,C9:],[:D,D9:]
let T9 be Functor of C9,D9; :: thesis: [:T,T9:] is Functor of [:C,C9:],[:D,D9:]
[:T,T9:] = <:(T * (pr1 (C,C9))),(T9 * (pr2 (C,C9))):> by Th64;
hence [:T,T9:] is Functor of [:C,C9:],[:D,D9:] ; :: thesis: verum