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 that
A1: len A = len B and
A2: width A = 0 and
A3: width B = 0 ; :: thesis: A = B
Seg (width A) = {} by A2;
then Indices A = {} by A2, ZFMISC_1:113;
then for i, j being Nat st [i,j] in Indices A holds
A * i,j = B * i,j by A2, FINSEQ_1:4, ZFMISC_1:113;
hence A = B by A1, A2, A3, MATRIX_1:21; :: thesis: verum