let D be non empty set ; :: thesis: for A being Matrix of D holds Segm A,(Seg (len A)),(Seg (width A)) = A
let A be Matrix of D; :: thesis: Segm A,(Seg (len A)),(Seg (width A)) = A
( Sgm (Seg (len A)) = idseq (len A) & Sgm (Seg (width A)) = idseq (width A) ) by FINSEQ_3:54;
hence Segm A,(Seg (len A)),(Seg (width A)) = A by Th42; :: thesis: verum