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