let m be Nat; :: thesis: for D being non empty set
for M being Matrix of 0 ,m,D holds
( len M = 0 & width M = 0 & Indices M = {} )
let D be non empty set ; :: thesis: for M being Matrix of 0 ,m,D holds
( len M = 0 & width M = 0 & Indices M = {} )
let M be Matrix of 0 ,m,D; :: thesis: ( len M = 0 & width M = 0 & Indices M = {} )
len M = 0 by Def2;
then width M = 0 by Def3;
then Seg (width M) = 0 ;
hence ( len M = 0 & width M = 0 & Indices M = {} ) by Def2, ZFMISC_1:90; :: thesis: verum