the carrier of (product J) = product (Carrier J) by Def3;
hence product J is constituted-Functions by MONOID_0:80; :: thesis: verum