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