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 ) by Def26, Def27; :: thesis: verum