the carrier of (max-Prod2 (M,N)) = [: the carrier of M, the carrier of N:] by Def1;
hence x `1 is Element of M by MCART_1:10; :: thesis: verum