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