the carrier of (product J) = product (Carrier J) by YELLOW_1:def 4;
hence product J is constituted-Functions by MONOID_0:89; :: thesis: verum