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