the ObjectMap of F is Covariant by Def12;
then consider f being Function of the carrier of C1, the carrier of C2 such that
A1: the ObjectMap of F = [:f,f:] ;
the ObjectMap of G is Covariant by Def12;
then consider g being Function of the carrier of C2, the carrier of C3 such that
A2: the ObjectMap of G = [:g,g:] ;
take g * f ; :: according to FUNCTOR0:def 1,FUNCTOR0:def 12 :: 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 Def36
.= [:(g * f),(g * f):] by A1, A2, FUNCT_3:71 ; :: thesis: verum