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_0:51;
reconsider M1 = M1 as Matrix of len A, width A,K by A6, MATRIX_0:51;
reconsider A1 = A as Matrix of len A, width A,K by MATRIX_0:51;
A10: Indices A1 = [:(Seg (len A)),(Seg (width A)):] by MATRIX_0:25;
A11: ( Indices M1 = [:(Seg (len A)),(Seg (width M1)):] & Indices M2 = [:(Seg (len A)),(Seg (width M2)):] ) by MATRIX_0:25;

A12: now :: thesis: ( ( len A > 0 & Indices A = Indices M1 & Indices M1 = Indices M2 ) or ( len A = 0 & Indices A = Indices M1 & Indices M1 = Indices M2 ) )

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_0:23;
hence ( Indices A = Indices M1 & Indices M1 = Indices M2 ) by A10, A13, MATRIX_0:23; :: thesis: verum

end;

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

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

end;

end;

end;

now :: thesis: for i, j being Nat st [i,j] in Indices A holds
M1 * (i,j) = M2 * (i,j)

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_0:27; :: thesis: verum