let D be non empty set ; :: thesis: for m, n 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 m, n 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_0:def 6;
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 :: thesis: for i, j being Nat st [i,j] in Indices ((Segm (A,nt,mt)) @) holds
((Segm (A,nt,mt)) @) * (i,j) = (Segm ((A @),mt,nt)) * (i,j)

A9: Indices (Segm ((A @),mt,nt)) = [:(Seg m),(Seg n):] by A7, MATRIX_0:25;
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 12;
A11: [j9,i9] in Indices (Segm (A,nt,mt)) by A10, MATRIX_0:def 6;
then A12: ((Segm (A,nt,mt)) @) * (i9,j9) = (Segm (A,nt,mt)) * (j9,i9) by MATRIX_0:def 6;
Indices (Segm (A,nt,mt)) = [:(Seg n),(Seg m):] by A6, MATRIX_0:25;
then A13: j9 in Seg n by A11, ZFMISC_1:87;
i9 in Seg m by A6, A11, ZFMISC_1:87;
then A14: [i9,j9] in Indices (Segm ((A @),mt,nt)) by A13, A9, ZFMISC_1:87;
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_0:def 6;
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_0:54;
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_0:21, MATRIX_0:54; :: thesis: verum

end;

end;