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 ZFMISC_1:90;
then for i, j being Nat st [i,j] in Indices A holds
A * (i,j) = B * (i,j) ;
hence A = B by A1, A2, A3, MATRIX_0:21; :: thesis: verum