consider o being object of C2;
take C1 --> (idm o) ; :: thesis: ( C1 --> (idm o) is feasible & C1 --> (idm o) is id-preserving & ( ( C1 --> (idm o) is Covariant & C1 --> (idm o) is comp-preserving ) or ( C1 --> (idm o) is Contravariant & C1 --> (idm o) is comp-reversing ) ) )
thus ( C1 --> (idm o) is feasible & C1 --> (idm o) is id-preserving & ( ( C1 --> (idm o) is Covariant & C1 --> (idm o) is comp-preserving ) or ( C1 --> (idm o) is Contravariant & C1 --> (idm o) is comp-reversing ) ) ) ; :: thesis: verum