consider o being object of B;
reconsider F = A --> (idm o) as Functor of A,B by Def26;
take F ; :: thesis: ( F is strict & F is covariant & F is contravariant & F is feasible )
thus ( F is strict & F is covariant & F is contravariant & F is feasible ) by Def27, Def28; :: thesis: verum