set FG = F * G;
reconsider FG = F * G as PartFunc of the carrier of C, the carrier of E ;
( ( C is empty or not D is empty ) & ( D is empty or not E is empty ) ) by A1, Th29;
hence F * G is Functor of C,E ; :: thesis: verum