the ObjectMap of F is Contravariant by Def14;
then consider f being Function of the carrier of C1,the carrier of C2 such that
A1: the ObjectMap of F = ~ [:f,f:] by Def3;
the ObjectMap of G is Contravariant by Def14;
then consider g being Function of the carrier of C2,the carrier of C3 such that
A2: the ObjectMap of G = ~ [:g,g:] by Def3;
take g * f ; :: according to FUNCTOR0:def 2,FUNCTOR0:def 13 :: thesis: the ObjectMap of (G * F) = [:(g * f),(g * f):]
thus the ObjectMap of (G * F) = the ObjectMap of G * the ObjectMap of F by Def37
.= ~ ((~ [:g,g:]) * [:f,f:]) by A1, A2, ALTCAT_2:2
.= ~ (~ ([:g,g:] * [:f,f:])) by ALTCAT_2:3
.= [:g,g:] * [:f,f:] by FUNCT_4:54
.= [:(g * f),(g * f):] by FUNCT_3:92 ; :: thesis: verum