A1: ( width (A + B) = width A & len A = n ) by MATRIX_0:def 2, MATRIX_3:def 3;
A2: len (A + B) = len A by MATRIX_3:def 3;

per cases ( n = 0 or n > 0 ) ;

suppose A3: n = 0 ; :: thesis: A + B is Matrix of n,m,K

then A + B = {} by A2, MATRIX_0:def 2;
hence A + B is Matrix of n,m,K by A3, MATRIX_0:13; :: thesis: verum

end;

suppose n > 0 ; :: thesis: A + B is Matrix of n,m,K

then width A = m by MATRIX_0:23;
hence A + B is Matrix of n,m,K by A2, A1, MATRIX_0:51; :: thesis: verum

end;

end;