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):] )
A2: Seg (len M) = dom M by FINSEQ_1:def 3;
len M = n by Def3;
hence ( len M = n & width M = m & Indices M = [:(Seg n),(Seg m):] ) by A1, A2, Th20; :: thesis: verum