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 & A --> (idm o) is id-preserving )
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 & A --> (idm o) is id-preserving ) ; :: thesis: verum