take Funct C,D ; :: thesis: for x being Element of Funct C,D holds x is Functor of C,D
thus for x being Element of Funct C,D holds x is Functor of C,D by Def2; :: thesis: verum