[:T,T9:] = <:(T * (pr1 (C,C9))),(T9 * (pr2 (C,C9))):> by Th39;
hence [:T,T9:] is Functor of [:C,C9:],[:D,D9:] ; :: thesis: verum