consider o being object of B;
take A --> (idm o) ; :: thesis: ( A --> (idm o) is strict & A --> (idm o) is comp-preserving & A --> (idm o) is comp-reversing & A --> (idm o) is Covariant & A --> (idm o) is Contravariant & A --> (idm o) is feasible )
thus ( A --> (idm o) is strict & A --> (idm o) is comp-preserving & A --> (idm o) is comp-reversing & A --> (idm o) is Covariant & A --> (idm o) is Contravariant & A --> (idm o) is feasible ) ; :: thesis: verum