consider o being object of B;
set I = A --> (idm o);
A --> (idm o) is Functor of A,B

proof

thus ( A --> (idm o) is feasible & A --> (idm o) is id-preserving & ( ( A --> (idm o) is Covariant & A --> (idm o) is comp-preserving ) or ( A --> (idm o) is Contravariant & A --> (idm o) is comp-reversing ) ) ) ; :: according to FUNCTOR0:def 26 :: thesis: verum

end;

then reconsider I = A --> (idm o) as Functor of A,B ;
take I ; :: thesis: ( I is strict & I is feasible & I is covariant & I is contravariant )
thus ( I is strict & I is feasible ) ; :: thesis: ( I is covariant & I is contravariant )
thus I is covariant ; :: thesis: I is contravariant
thus I is contravariant ; :: thesis: verum