theorem :: MATRIX_0:22

for m being Nat
for D being non empty set
for M being Matrix of 0 ,m,D holds
( len M = 0 & width M = 0 & Indices M = {} )