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

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