the ObjectMap of F is Contravariant
by Def13;
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
; FUNCTOR0:def 2,FUNCTOR0:def 13 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,g:] * [:f,f:])
by A1, A2, ALTCAT_2:2
.=
~ [:(g * f),(g * f):]
by FUNCT_3:71
; verum