let m be Nat; :: thesis: for D being non empty set holds {} is Matrix of 0 ,m,D
let D be non empty set ; :: thesis: {} is Matrix of 0 ,m,D
reconsider M = <*> (D *) as FinSequence of D * ;
reconsider M = M as Matrix of D by Th5;
M is Matrix of 0 ,m,D

proof

thus len M = 0 ; :: according to MATRIX_1:def 2 :: thesis: for p being FinSequence of D st p in rng M holds
len p = m
let p be FinSequence of D; :: thesis: ( p in rng M implies len p = m )
assume p in rng M ; :: thesis: len p = m
hence len p = m ; :: thesis: verum

end;

hence {} is Matrix of 0 ,m,D ; :: thesis: verum