set n = len A;
let M1, M2 be Matrix of K; :: thesis: ( len M1 = len A & width M1 = width A & ( for i, j being Nat st [i,j] in Indices A holds
M1 * i,j = (A * i,j) + (B * i,j) ) & len M2 = len A & width M2 = width A & ( for i, j being Nat st [i,j] in Indices A holds
M2 * i,j = (A * i,j) + (B * i,j) ) implies M1 = M2 )
assume that
A6: ( len M1 = len A & width M1 = width A ) and
A7: for i, j being Nat st [i,j] in Indices A holds
M1 * i,j = (A * i,j) + (B * i,j) and
A8: ( len M2 = len A & width M2 = width A ) and
A9: for i, j being Nat st [i,j] in Indices A holds
M2 * i,j = (A * i,j) + (B * i,j) ; :: thesis: M1 = M2
reconsider M2 = M2 as Matrix of len A, width A,K by A8, MATRIX_2:7;
reconsider M1 = M1 as Matrix of len A, width A,K by A6, MATRIX_2:7;
reconsider A1 = A as Matrix of len A, width A,K by MATRIX_2:7;
A10: Indices A1 = [:(Seg (len A)),(Seg (width A)):] by MATRIX_1:26;
A11: ( Indices M1 = [:(Seg (len A)),(Seg (width M1)):] & Indices M2 = [:(Seg (len A)),(Seg (width M2)):] ) by MATRIX_1:26;

A12: now

per cases ( len A > 0 or len A = 0 ) ;

case A13: len A > 0 ; :: thesis: ( Indices A = Indices M1 & Indices M1 = Indices M2 )

then Indices M1 = [:(Seg (len A)),(Seg (width A)):] by MATRIX_1:24;
hence ( Indices A = Indices M1 & Indices M1 = Indices M2 ) by A10, A13, MATRIX_1:24; :: thesis: verum

end;

case A14: len A = 0 ; :: thesis: ( Indices A = Indices M1 & Indices M1 = Indices M2 )

then len M1 = 0 by MATRIX_1:def 3;
then A15: width M1 = 0 by MATRIX_1:def 4;
len M2 = 0 by A14, MATRIX_1:def 3;
hence ( Indices A = Indices M1 & Indices M1 = Indices M2 ) by A10, A11, A14, A15, MATRIX_1:def 4; :: thesis: verum

end;

end;

end;

now

let i, j be Nat; :: thesis: ( [i,j] in Indices A implies M1 * i,j = M2 * i,j )
assume A16: [i,j] in Indices A ; :: thesis: M1 * i,j = M2 * i,j
then M1 * i,j = (A * i,j) + (B * i,j) by A7;
hence M1 * i,j = M2 * i,j by A9, A16; :: thesis: verum

end;

hence M1 = M2 by A12, MATRIX_1:28; :: thesis: verum