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

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