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