let D be non empty set ; :: thesis: for A, B being Matrix of D st len A = len B & width A = 0 & width B = 0 holds
A = B
let A, B be Matrix of D; :: thesis: ( len A = len B & width A = 0 & width B = 0 implies A = B )
assume A1: ( len A = len B & width A = 0 & width B = 0 ) ; :: thesis: A = B
for i, j being Nat st [i,j] in Indices A holds
A * i,j = B * i,j by A1, FINSEQ_1:4, ZFMISC_1:113;
hence A = B by A1, MATRIX_1:21; :: thesis: verum