let D be non empty set ; :: thesis:
let m, n be Nat; :: thesis:
let A be Matrix of D; :: thesis:
let nt be Element of n -tuples_on NAT ; :: thesis:
let mt be Element of m -tuples_on NAT ; :: thesis:
assume that
A1: [:(rng nt),(rng mt):] c= Indices A and
A2: ( m = 0 implies n = 0 ) ; :: thesis:
set S = Segm A,nt,mt;
set S' = Segm (A @ ),mt,nt;

per cases ;

suppose A3: n = 0 ; :: thesis:

( len (Segm (A @ ),mt,nt) = 0 or ( len (Segm (A @ ),mt,nt) > 0 & len (Segm (A @ ),mt,nt) = m ) ) by MATRIX_1:def 3;
then ( width (Segm (A @ ),mt,nt) = 0 & len (Segm A,nt,mt) = 0 ) by A3, MATRIX_1:24, MATRIX_1:def 3, MATRIX_1:def 4;
then ( len ((Segm (A @ ),mt,nt) @ ) = 0 & Segm A,nt,mt = {} ) by MATRIX_1:def 7;
hence Segm A,nt,mt = (Segm (A @ ),mt,nt) @ ; :: thesis:

end;

suppose A4: n > 0 ; :: thesis:

then ( len (Segm A,nt,mt) = n & width (Segm A,nt,mt) = m & m > 0 ) by A2, Th1;
then ( ((Segm A,nt,mt) @ ) @ = Segm A,nt,mt & width ((Segm A,nt,mt) @ ) = n & (Segm A,nt,mt) @ = Segm (A @ ),mt,nt ) by A1, A4, Th18, MATRIX_2:12, MATRIX_2:15;
hence Segm A,nt,mt = (Segm (A @ ),mt,nt) @ ; :: thesis:

end;