let D be non empty set ; :: thesis: for n, m being Nat
for A being Matrix of D
for nt being Element of n -tuples_on NAT
for mt being Element of m -tuples_on NAT holds
not ( [:(rng nt),(rng mt):] c= Indices A & ( n = 0 implies m = 0 ) & ( m = 0 implies n = 0 ) & not (Segm A,nt,mt) @ = Segm (A @ ),mt,nt )
let n, m be Nat; :: thesis: for A being Matrix of D
for nt being Element of n -tuples_on NAT
for mt being Element of m -tuples_on NAT holds
not ( [:(rng nt),(rng mt):] c= Indices A & ( n = 0 implies m = 0 ) & ( m = 0 implies n = 0 ) & not (Segm A,nt,mt) @ = Segm (A @ ),mt,nt )
let A be Matrix of D; :: thesis: for nt being Element of n -tuples_on NAT
for mt being Element of m -tuples_on NAT holds
not ( [:(rng nt),(rng mt):] c= Indices A & ( n = 0 implies m = 0 ) & ( m = 0 implies n = 0 ) & not (Segm A,nt,mt) @ = Segm (A @ ),mt,nt )
let nt be Element of n -tuples_on NAT ; :: thesis: for mt being Element of m -tuples_on NAT holds
not ( [:(rng nt),(rng mt):] c= Indices A & ( n = 0 implies m = 0 ) & ( m = 0 implies n = 0 ) & not (Segm A,nt,mt) @ = Segm (A @ ),mt,nt )
let mt be Element of m -tuples_on NAT ; :: thesis: not ( [:(rng nt),(rng mt):] c= Indices A & ( n = 0 implies m = 0 ) & ( m = 0 implies n = 0 ) & not (Segm A,nt,mt) @ = Segm (A @ ),mt,nt )
assume that
A1: [:(rng nt),(rng mt):] c= Indices A and
A2: ( n = 0 iff m = 0 ) ; :: thesis: (Segm A,nt,mt) @ = Segm (A @ ),mt,nt
set A9 = A @ ;
set SA = Segm A,nt,mt;
set SA9 = Segm (A @ ),mt,nt;

per cases ( n = 0 or n > 0 ) ;

suppose A3: n = 0 ; :: thesis: (Segm A,nt,mt) @ = Segm (A @ ),mt,nt

then width (Segm A,nt,mt) = 0 by A2, Th1;
then len ((Segm A,nt,mt) @ ) = 0 by MATRIX_1:def 7;
then A4: (Segm A,nt,mt) @ = {} ;
len (Segm (A @ ),mt,nt) = 0 by A2, A3, Th1;
hence (Segm A,nt,mt) @ = Segm (A @ ),mt,nt by A4; :: thesis: verum

end;

suppose A5: n > 0 ; :: thesis: (Segm A,nt,mt) @ = Segm (A @ ),mt,nt

then A6: width (Segm A,nt,mt) = m by Th1;
A7: width (Segm (A @ ),mt,nt) = n by A2, Th1;

A8: now

A9: Indices (Segm (A @ ),mt,nt) = [:(Seg m),(Seg n):] by A7, MATRIX_1:26;
let i, j be Nat; :: thesis: ( [i,j] in Indices ((Segm A,nt,mt) @ ) implies ((Segm A,nt,mt) @ ) * i,j = (Segm (A @ ),mt,nt) * i,j )
assume A10: [i,j] in Indices ((Segm A,nt,mt) @ ) ; :: thesis: ((Segm A,nt,mt) @ ) * i,j = (Segm (A @ ),mt,nt) * i,j
reconsider i9 = i, j9 = j as Element of NAT by ORDINAL1:def 13;
A11: [j9,i9] in Indices (Segm A,nt,mt) by A10, MATRIX_1:def 7;
then A12: ((Segm A,nt,mt) @ ) * i9,j9 = (Segm A,nt,mt) * j9,i9 by MATRIX_1:def 7;
Indices (Segm A,nt,mt) = [:(Seg n),(Seg m):] by A6, MATRIX_1:26;
then A13: j9 in Seg n by A11, ZFMISC_1:106;
i9 in Seg m by A6, A11, ZFMISC_1:106;
then A14: [i9,j9] in Indices (Segm (A @ ),mt,nt) by A13, A9, ZFMISC_1:106;
A15: (Segm A,nt,mt) * j9,i9 = A * (nt . j),(mt . i) by A11, Def1;
[(nt . j),(mt . i)] in Indices A by A1, A11, Th17;
then ((Segm A,nt,mt) @ ) * i9,j9 = (A @ ) * (mt . i),(nt . j) by A15, A12, MATRIX_1:def 7;
hence ((Segm A,nt,mt) @ ) * i,j = (Segm (A @ ),mt,nt) * i,j by A14, Def1; :: thesis: verum

end;

len (Segm (A @ ),mt,nt) = m by A2, Th1;
then A16: len ((Segm A,nt,mt) @ ) = len (Segm (A @ ),mt,nt) by A2, A5, A6, MATRIX_2:12;
len (Segm A,nt,mt) = n by A5, Th1;
hence (Segm A,nt,mt) @ = Segm (A @ ),mt,nt by A2, A5, A6, A7, A16, A8, MATRIX_1:21, MATRIX_2:12; :: thesis: verum

end;

end;