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