G * F is Functor of A,C

proof

thus ( G * F is feasible & G * F is id-preserving ) ; :: according to FUNCTOR0:def 26 :: thesis: ( ( G * F is Covariant & G * F is comp-preserving ) or ( G * F is Contravariant & G * F is comp-reversing ) )
thus ( ( G * F is Covariant & G * F is comp-preserving ) or ( G * F is Contravariant & G * F is comp-reversing ) ) ; :: thesis: verum

end;

then reconsider GF = G * F as Functor of A,C ;
GF is covariant ;
hence G * F is strict covariant Functor of A,C ; :: thesis: verum