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