product (Carrier J) is functional ;
hence the carrier of (product J) is functional by YELLOW_1:def 4; :: thesis: verum