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 18;
hence ( o is Object of (Functors A,B) iff o is Functor of A,B ) by CAT_2:def 2; :: thesis: verum