A1: the carrier of (product F) = product (Carrier F) by Def2;
hence not the carrier of (product F) is empty ; :: according to STRUCT_0:def 1 :: thesis: product F is constituted-Functions
thus product F is constituted-Functions by A1, MONOID_0:80; :: thesis: verum