let n, m be Nat; :: thesis: for D being non empty set st n > 0 holds
for M being Matrix of n,m,D holds
( len M = n & width M = m & Indices M = [:(Seg n),(Seg m):] )
let D be non empty set ; :: thesis: ( n > 0 implies for M being Matrix of n,m,D holds
( len M = n & width M = m & Indices M = [:(Seg n),(Seg m):] ) )
assume A1: n > 0 ; :: thesis: for M being Matrix of n,m,D holds
( len M = n & width M = m & Indices M = [:(Seg n),(Seg m):] )
let M be Matrix of n,m,D; :: thesis: ( len M = n & width M = m & Indices M = [:(Seg n),(Seg m):] )
( Seg (len M) = dom M & len M = n ) by Def2, FINSEQ_1:def 3;
hence ( len M = n & width M = m & Indices M = [:(Seg n),(Seg m):] ) by A1, Th20; :: thesis: verum