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 0 ,m -size ;
hence {} is Matrix of 0 ,m,D ; :: thesis: verum