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

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