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