set o = the Object of B;

set I = A --> (idm the Object of B);

reconsider I = A --> (idm the Object of B) as Functor of A,B by FUNCTOR0:def 25;

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

set I = A --> (idm the Object of B);

reconsider I = A --> (idm the Object of B) as Functor of A,B by FUNCTOR0:def 25;

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