A1:
width M2 = n
by MATRIX_0:24;

width M1 = n by MATRIX_0:24;

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_0:24, MATRIX_0:51; :: thesis: verum

width M1 = n by MATRIX_0:24;

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_0:24, MATRIX_0:51; :: thesis: verum