let D, E be non empty set ; :: thesis: for n, m being Nat
for M being Matrix of n,m,D st ( for i, j being Nat st [i,j] in Indices M holds
M * (i,j) in E ) holds
M is Matrix of n,m,E
let n, m be Nat; :: thesis: for M being Matrix of n,m,D st ( for i, j being Nat st [i,j] in Indices M holds
M * (i,j) in E ) holds
M is Matrix of n,m,E
let M be Matrix of n,m,D; :: thesis: ( ( for i, j being Nat st [i,j] in Indices M holds
M * (i,j) in E ) implies M is Matrix of n,m,E )
assume for i, j being Nat st [i,j] in Indices M holds
M * (i,j) in E ; :: thesis: M is Matrix of n,m,E
then reconsider G = M as Matrix of E by ZMATRLIN:5;

per cases ( not n > 0 or n > 0 ) ;

suppose not n > 0 ; :: thesis: M is Matrix of n,m,E

then X1: n = 0 ;
then G = {} by MATRIX_0:22;
hence M is Matrix of n,m,E by X1, MATRIX_0:13; :: thesis: verum

end;

suppose X1: n > 0 ; :: thesis: M is Matrix of n,m,E

then ( len G = n & width G = m ) by MATRIX_0:23;
hence M is Matrix of n,m,E by X1, MATRIX_0:20; :: thesis: verum

end;

end;