let x be Element of Funct (C,D); :: according to CAT_2:def 3 :: thesis: x is Functor of C,D
thus x is Functor of C,D by Def2; :: thesis: verum