consider f being Covariant 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 Covariant
thus the ObjectMap of F is Covariant ; :: according to FUNCTOR0:def 13 :: thesis: verum