let n, m be Nat; 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 ; 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; ( 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; verum