A1: width M2 = n by MATRIX_1:25;
width M1 = n by MATRIX_1:25;
then ( len (M1 + M2) = len M1 & width (M1 + M2) = width M2 ) by A1, MATRIX_3:def 3;
hence M1 + M2 is Matrix of n, REAL by A1, MATRIX_1:25, MATRIX_2:7; :: thesis: verum