let K be Field; :: thesis: for A, B being Matrix of K holds Indices (A + B) = Indices A
let A, B be Matrix of K; :: thesis: Indices (A + B) = Indices A
( len (A + B) = len A & width (A + B) = width A ) by MATRIX_3:def 3;
hence Indices (A + B) = Indices A by MATRIX_4:55; :: thesis: verum