let A, B be Category; :: thesis: for o being set holds
( o is Object of (Functors (A,B)) iff o is Functor of A,B )
let o be set ; :: thesis: ( o is Object of (Functors (A,B)) iff o is Functor of A,B )
the carrier of (Functors (A,B)) = Funct (A,B) by NATTRA_1:def 17;
hence ( o is Object of (Functors (A,B)) iff o is Functor of A,B ) by CAT_2:def 2; :: thesis: verum