consider f being Contravariant bifunction of the carrier of C1, the carrier of C2;
consider M being MSUnTrans of f, the Arrows of C1, the Arrows of C2;
take F = FunctorStr(# f,M #); :: thesis: F is Contravariant
thus the ObjectMap of F is Contravariant ; :: according to FUNCTOR0:def 14 :: thesis: verum