set o = the Object of B;
reconsider F = A --> (idm the Object of B) as Functor of A,B by Def25;
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 ) ; :: thesis: verum