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
A1: Sgm (Seg (width A)) = idseq (width A) by FINSEQ_3:48;
Sgm (Seg (len A)) = idseq (len A) by FINSEQ_3:48;
hence Segm (A,(Seg (len A)),(Seg (width A))) = A by A1, Th42; :: thesis: verum